equal
deleted
inserted
replaced
70 fun std_postprocessor ss = |
70 fun std_postprocessor ss = |
71 Prim.postprocess |
71 Prim.postprocess |
72 {WFtac = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, |
72 {WFtac = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, |
73 wf_less_than, wf_trancl] 1), |
73 wf_less_than, wf_trancl] 1), |
74 terminator = asm_simp_tac ss 1 |
74 terminator = asm_simp_tac ss 1 |
75 THEN TRY(best_tac |
75 THEN TRY(CLASET' (fn cs => best_tac |
76 (!claset addSDs [not0_implies_Suc] addss ss) 1), |
76 (cs addSDs [not0_implies_Suc] addss ss)) 1), |
77 simplifier = Rules.simpl_conv ss []}; |
77 simplifier = Rules.simpl_conv ss []}; |
78 |
78 |
79 |
79 |
80 |
80 |
81 val concl = #2 o Rules.dest_thm; |
81 val concl = #2 o Rules.dest_thm; |