さて，rewritingは数学においてごく普通の処理ですから，HOL Lightは，複数のtheoremsを合わせて参照する，より高度なrewriting conversionを提供します． その最も一般的なものが GEN_REWRITE_CONV convl [th1; ...; thn] (: (conv -> conv) -> thm list ->…

このREWR_CONV(: thm -> term -> thm = )を先のdepth conversions(: conv -> conv = )のもとで用いれば，等式についてのtheoremから導ける限りのtermの書き換えが可能になります． 例えば # let tm = `(a + b) + ((c + d) + e) + f + g + h` ;; val tm : ter…