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.
arith_tac should not produce counter example
authornipkow
Tue, 13 Aug 2002 22:01:53 +0200
changeset 13501 79242cccaddc
parent 13500 2222c7a0e8bb
child 13502 da43ebc02f17
arith_tac should not produce counter example
TFL/post.ML file | annotate | diff | comparison | revisions 
--- a/TFL/post.ML	Tue Aug 13 21:59:44 2002 +0200
+++ b/TFL/post.ML	Tue Aug 13 22:01:53 2002 +0200
@@ -71,7 +71,7 @@
   Prim.postprocess strict
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
-                 THEN TRY (arith_tac 1 ORELSE
+                 THEN TRY (silent_arith_tac 1 ORELSE
                            fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};
isabelle