| changeset 9907 | 473a6604da94 |
| parent 9303 | f1ad1ed0d110 |
| child 11695 | 8c66866fb0ff |
--- a/src/ZF/equalities.ML Thu Sep 07 21:10:11 2000 +0200 +++ b/src/ZF/equalities.ML Thu Sep 07 21:12:49 2000 +0200 @@ -29,7 +29,7 @@ Goal "[| a: C; ALL y:C. y=b |] ==> C = {b}"; by (Blast_tac 1); qed "equal_singleton_lemma"; -val equal_singleton = ballI RSN (2,equal_singleton_lemma); +bind_thm ("equal_singleton", ballI RSN (2,equal_singleton_lemma)); (** Binary Intersection **)