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.
Fixed a bug in the EX simproc.
authornipkow
Wed, 27 Oct 1999 17:17:28 +0200
changeset 7951 b36913c35699
parent 7950 720af28e6354
child 7952 43d3e087688c
Fixed a bug in the EX simproc.
src/Provers/quantifier1.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/quantifier1.ML	Wed Oct 27 17:09:31 1999 +0200
+++ b/src/Provers/quantifier1.ML	Wed Oct 27 17:17:28 1999 +0200
@@ -102,9 +102,10 @@
           in Some(prove_conv prove_all_tac sg (F,all$Abs(x,T,R))) end)
   | rearrange_all _ _ _ = None;
 
+(* Better: instantiate exI *)
 val prove_ex_tac = rtac iffI 1 THEN
-    ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
-                    rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)]);
+    ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
+                    DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
 
 fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
      (case extract P of
isabelle