CHANGED_CONV : conv -> conv
# ONCE_DEPTH_CONV num_CONV `x + 0`;; val it : thm = |- x + 0 = x + 0 # CHANGED_CONV(ONCE_DEPTH_CONV num_CONV) `x + 0`;; Exception: Failure "CHANGED_CONV". # CHANGED_CONV(ONCE_DEPTH_CONV num_CONV) `6`;; val it : thm = |- 6 = SUC 5 # REPEATC(CHANGED_CONV(ONCE_DEPTH_CONV num_CONV)) `6`;; val it : thm = |- 6 = SUC (SUC (SUC (SUC (SUC (SUC 0)))))