author | nipkow |
Thu, 13 Dec 2001 16:48:07 +0100 | |
changeset 12488 | 83acab8042ad |
parent 12487 | bbd564190c9b |
child 12489 | c92e38c3cbaa |
TFL/post.ML | file | annotate | diff | comparison | revisions |
--- a/TFL/post.ML Thu Dec 13 16:47:35 2001 +0100 +++ b/TFL/post.ML Thu Dec 13 16:48:07 2001 +0100 @@ -71,7 +71,8 @@ Prim.postprocess strict {wf_tac = REPEAT (ares_tac wfs 1), terminator = asm_simp_tac ss 1 - THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), + THEN TRY (arith_tac 1 ORELSE + fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), simplifier = Rules.simpl_conv ss []};