equal
deleted
inserted
replaced
66 *--------------------------------------------------------------------------*) |
66 *--------------------------------------------------------------------------*) |
67 fun std_postprocessor strict cs ss wfs = |
67 fun std_postprocessor strict cs ss wfs = |
68 Prim.postprocess strict |
68 Prim.postprocess strict |
69 {wf_tac = REPEAT (ares_tac wfs 1), |
69 {wf_tac = REPEAT (ares_tac wfs 1), |
70 terminator = asm_simp_tac ss 1 |
70 terminator = asm_simp_tac ss 1 |
71 THEN TRY (silent_arith_tac 1 ORELSE |
71 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE |
72 fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), |
72 fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), |
73 simplifier = Rules.simpl_conv ss []}; |
73 simplifier = Rules.simpl_conv ss []}; |
74 |
74 |
75 |
75 |
76 |
76 |