ループする REWRITE たち

例えば

# REAL_NEG_MINUS1;;
val it : thm = |- !x. --x = -- &1 * x

を `-- x` に適用しようと

# REWRITE_CONV [REAL_NEG_MINUS1] `-- x`;;

としても．．．帰ってきません．

これは等式の右辺の -- &1 にも同じ書き換えが適用され，ループに陥っている為です．したがって

# ONCE_REWRITE_CONV [REAL_NEG_MINUS1] `-- x`;;
val it : thm = |- --x = -- &1 * x
# funpow 3 (rand o concl o (ONCE_REWRITE_CONV [REAL_NEG_MINUS1])) `-- x`
;;
val it : term = `((-- &1 * &1) * &1) * x`

のようにします．