| changeset 5266 | 1d11c7e4b999 |
| parent 5256 | e6983301ce5e |
| child 5305 | 513925de8962 |
--- 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);