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 name: UN_empty3;
authorwenzelm
Thu, 13 Jul 2000 23:10:12 +0200
changeset 9312 a93a7b6bb654
parent 9311 ab5b24cbaa16
child 9313 b5a29408dc39
fixed name: UN_empty3;
src/HOL/equalities.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/equalities.ML	Thu Jul 13 23:09:25 2000 +0200
+++ b/src/HOL/equalities.ML	Thu Jul 13 23:10:12 2000 +0200
@@ -592,8 +592,8 @@
 
 Goal "(UNION A B = {}) = (ALL x:A. B x = {})";
 by Auto_tac; 
-qed "UN_empty";
-AddIffs [UN_empty];
+qed "UN_empty3";
+AddIffs [UN_empty3];
 
 
 (*Distributive laws...*)
isabelle