| changeset 9399 | effc8d44c89c |
| parent 9338 | fcf7f29a3447 |
| child 9422 | 4b6bc2b347e5 |
--- a/src/HOL/equalities.ML Fri Jul 21 17:41:59 2000 +0200 +++ b/src/HOL/equalities.ML Fri Jul 21 17:46:29 2000 +0200 @@ -354,10 +354,6 @@ by (blast_tac (claset() addSEs [equalityCE]) 1); qed "subset_Un_eq"; -Goal "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)"; -by (Blast_tac 1); -qed "subset_insert_iff"; - Goal "(A Un B = {}) = (A = {} & B = {})"; by (blast_tac (claset() addEs [equalityCE]) 1); qed "Un_empty";