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.
Now recognizes both {}= and ={}
authorpaulson
Thu, 06 Aug 1998 10:47:13 +0200
changeset 5266 1d11c7e4b999
parent 5265 9d1d4c43c76d
child 5267 41a01176b9de
Now recognizes both {}= and ={}
src/HOL/Set.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.ML	Thu Aug 06 10:38:57 1998 +0200
+++ b/src/HOL/Set.ML	Thu Aug 06 10:47:13 1998 +0200
@@ -263,7 +263,7 @@
 qed_goal "equals0E" Set.thy "!!a. [| A={};  a:A |] ==> P"
  (fn _ => [ (Blast_tac 1) ]);
 
-AddEs [equals0E];
+AddEs [equals0E, sym RS equals0E];
 
 Goalw [Ball_def] "Ball {} P = True";
 by (Simp_tac 1);
isabelle