| changeset 26806 | 40b411ec05aa |
| parent 16417 | 9bc16273c2d4 |
| child 36745 | 403585a89772 |
| 26805:27941d7d9a11 | 26806:40b411ec05aa |
|---|---|
149 done |
149 done |
150 |
150 |
151 text{*Pow, Inter too little used*} |
151 text{*Pow, Inter too little used*} |
152 |
152 |
153 lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)" |
153 lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)" |
154 apply (simp add: psubset_def) |
154 apply (simp add: psubset_eq) |
155 done |
155 done |
156 |
156 |
157 end |
157 end |