src/ZF/int_arith.ML
changeset 40878 7695e4de4d86
parent 40313 54e8be8b4de0
child 44947 8ae418dfe561
--- a/src/ZF/int_arith.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/ZF/int_arith.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -312,7 +312,7 @@
 (*
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s; by (Asm_simp_tac 1));
 val sg = #sign (rep_thm (topthm()));
 val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));