Now recognizes both {}= and ={}
authorpaulson
Thu Aug 06 10:47:13 1998 +0200 (1998-08-06)
changeset 52661d11c7e4b999
parent 5265 9d1d4c43c76d
child 5267 41a01176b9de
Now recognizes both {}= and ={}
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Thu Aug 06 10:38:57 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Aug 06 10:47:13 1998 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4  qed_goal "equals0E" Set.thy "!!a. [| A={};  a:A |] ==> P"
     1.5   (fn _ => [ (Blast_tac 1) ]);
     1.6  
     1.7 -AddEs [equals0E];
     1.8 +AddEs [equals0E, sym RS equals0E];
     1.9  
    1.10  Goalw [Ball_def] "Ball {} P = True";
    1.11  by (Simp_tac 1);