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));