equal
deleted
inserted
replaced
261 |
261 |
262 (*Use for reasoning about disjointness: A Int B = {} *) |
262 (*Use for reasoning about disjointness: A Int B = {} *) |
263 qed_goal "equals0E" Set.thy "!!a. [| A={}; a:A |] ==> P" |
263 qed_goal "equals0E" Set.thy "!!a. [| A={}; a:A |] ==> P" |
264 (fn _ => [ (Blast_tac 1) ]); |
264 (fn _ => [ (Blast_tac 1) ]); |
265 |
265 |
266 AddEs [equals0E]; |
266 AddEs [equals0E, sym RS equals0E]; |
267 |
267 |
268 Goalw [Ball_def] "Ball {} P = True"; |
268 Goalw [Ball_def] "Ball {} P = True"; |
269 by (Simp_tac 1); |
269 by (Simp_tac 1); |
270 qed "ball_empty"; |
270 qed "ball_empty"; |
271 |
271 |