equal
deleted
inserted
replaced
27 qed "cons_Diff"; |
27 qed "cons_Diff"; |
28 |
28 |
29 Goal "[| a: C; ALL y:C. y=b |] ==> C = {b}"; |
29 Goal "[| a: C; ALL y:C. y=b |] ==> C = {b}"; |
30 by (Blast_tac 1); |
30 by (Blast_tac 1); |
31 qed "equal_singleton_lemma"; |
31 qed "equal_singleton_lemma"; |
32 val equal_singleton = ballI RSN (2,equal_singleton_lemma); |
32 bind_thm ("equal_singleton", ballI RSN (2,equal_singleton_lemma)); |
33 |
33 |
34 |
34 |
35 (** Binary Intersection **) |
35 (** Binary Intersection **) |
36 |
36 |
37 (*NOT an equality, but it seems to belong here...*) |
37 (*NOT an equality, but it seems to belong here...*) |