Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/UNITY/Constrains.thy
changeset 35409 5c5bb83f2bae
parent 32960 69916a850301
child 42793 88bee9f6eec7 
--- a/src/ZF/UNITY/Constrains.thy	Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Sun Feb 28 22:30:51 2010 +0100
@@ -484,9 +484,9 @@
               REPEAT (force_tac css 2),
               full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
               ALLGOALS (clarify_tac cs),
-              REPEAT (FIRSTGOAL (etac disjE)),
+              REPEAT (FIRSTGOAL (etac @{thm disjE})),
               ALLGOALS (clarify_tac cs),
-              REPEAT (FIRSTGOAL (etac disjE)),
+              REPEAT (FIRSTGOAL (etac @{thm disjE})),
               ALLGOALS (clarify_tac cs),
               ALLGOALS (asm_full_simp_tac ss),
               ALLGOALS (clarify_tac cs)])
isabelle