Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Terminator now uses arith_tac as well.
authornipkow
Thu, 13 Dec 2001 16:48:07 +0100
changeset 12488 83acab8042ad
parent 12487 bbd564190c9b
child 12489 c92e38c3cbaa
Terminator now uses arith_tac as well.
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 []};
isabelle