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.
Cla.swap;
authorwenzelm
Thu, 08 Dec 2005 20:15:41 +0100
changeset 18371 d93fdf00f8a6
parent 18370 db5900e7c6c9
child 18372 2bffdf62fe7f
Cla.swap;
src/CCL/Set.ML file | annotate | diff | comparison | revisions
src/ZF/UNITY/SubstAx.thy file | annotate | diff | comparison | revisions 
--- a/src/CCL/Set.ML	Thu Dec 08 20:15:34 2005 +0100
+++ b/src/CCL/Set.ML	Thu Dec 08 20:15:41 2005 +0100
@@ -234,7 +234,7 @@
 val emptyE = make_elim emptyD;
 
 val [prem] = goal (the_context ()) "~ A={} ==> (EX x. x:A)";
-by (rtac (prem RS swap) 1);
+by (rtac (prem RS Cla.swap) 1);
 by (rtac equalityI 1);
 by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
 qed "not_emptyD";
--- a/src/ZF/UNITY/SubstAx.thy	Thu Dec 08 20:15:34 2005 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Thu Dec 08 20:15:41 2005 +0100
@@ -416,7 +416,7 @@
                  (*simplify the command's domain*)
               simp_tac (ss addsimps [domain_def]) 3, 
               (* proving the domain part *)
-             clarify_tac cs 3, dtac swap 3, force_tac (cs,ss) 4,
+             clarify_tac cs 3, dtac Cla.swap 3, force_tac (cs,ss) 4,
              rtac ReplaceI 3, force_tac (cs,ss) 3, force_tac (cs,ss) 4,
              asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
              REPEAT (rtac state_update_type 3),
isabelle