| changeset 13172 | 03a5afa7b888 |
| parent 13169 | 394a6c649547 |
| child 13174 | 85d3c0981a16 |
--- a/src/ZF/equalities.thy Wed May 22 17:26:34 2002 +0200 +++ b/src/ZF/equalities.thy Wed May 22 18:11:57 2002 +0200 @@ -198,6 +198,8 @@ lemma equal_singleton [rule_format]: "[| a: C; ALL y:C. y=b |] ==> C = {b}" by blast +lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)" +by blast (** Binary Intersection **)