equal
deleted
inserted
replaced
53 *--------------------------------------------------------------------------*) |
53 *--------------------------------------------------------------------------*) |
54 fun std_postprocessor strict cs ss wfs = |
54 fun std_postprocessor strict cs ss wfs = |
55 Prim.postprocess strict |
55 Prim.postprocess strict |
56 {wf_tac = REPEAT (ares_tac wfs 1), |
56 {wf_tac = REPEAT (ares_tac wfs 1), |
57 terminator = asm_simp_tac ss 1 |
57 terminator = asm_simp_tac ss 1 |
58 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE |
58 THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE |
59 fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), |
59 fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), |
60 simplifier = Rules.simpl_conv ss []}; |
60 simplifier = Rules.simpl_conv ss []}; |
61 |
61 |
62 |
62 |
63 |
63 |