equal
deleted
inserted
replaced
67 * non-proved termination conditions, and finally attempts to prove the |
67 * non-proved termination conditions, and finally attempts to prove the |
68 * simplified termination conditions. |
68 * simplified termination conditions. |
69 *--------------------------------------------------------------------------*) |
69 *--------------------------------------------------------------------------*) |
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_empty, wf_measure, wf_inv_image, |
73 wf_less_than, wf_trancl] 1), |
73 wf_lex_prod, wf_less_than, wf_trancl] 1), |
74 terminator = asm_simp_tac ss 1 |
74 terminator = asm_simp_tac ss 1 |
75 THEN TRY(CLASET' (fn cs => best_tac |
75 THEN TRY(CLASET' (fn cs => best_tac |
76 (cs 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 |