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.
AddXEs [UnI1, UnI2];
authorwenzelm
Thu, 27 Sep 2001 16:04:25 +0200
changeset 11589 9a6d4511bb3c
parent 11588 d792570a04b1
child 11590 14ae6a86813d
AddXEs [UnI1, UnI2];
src/HOL/Set.ML file | annotate | diff | comparison | revisions
src/ZF/upair.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.ML	Thu Sep 27 16:04:11 2001 +0200
+++ b/src/HOL/Set.ML	Thu Sep 27 16:04:25 2001 +0200
@@ -422,7 +422,7 @@
 by (Asm_simp_tac 1);
 qed "UnI2";
 
-AddXIs [UnI1, UnI2];
+AddXEs [UnI1, UnI2];
 
 
 (*Classical introduction rule: no commitment to A vs B*)
--- a/src/ZF/upair.ML	Thu Sep 27 16:04:11 2001 +0200
+++ b/src/ZF/upair.ML	Thu Sep 27 16:04:25 2001 +0200
@@ -84,6 +84,7 @@
 
 AddSIs [UnCI];
 AddSEs [UnE];
+AddXEs [UnI1, UnI2];
 
 
 (*** Rules for small intersection -- Int -- defined via Upair ***)
isabelle