equal
deleted
inserted
replaced
217 by (rtac Ord_Least 1); |
217 by (rtac Ord_Least 1); |
218 qed "Card_is_Ord"; |
218 qed "Card_is_Ord"; |
219 |
219 |
220 goal Cardinal.thy "!!K. Card(K) ==> K le |K|"; |
220 goal Cardinal.thy "!!K. Card(K) ==> K le |K|"; |
221 by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); |
221 by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); |
222 val Card_cardinal_le = result(); |
222 qed "Card_cardinal_le"; |
223 |
223 |
224 goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; |
224 goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; |
225 by (rtac Ord_Least 1); |
225 by (rtac Ord_Least 1); |
226 qed "Ord_cardinal"; |
226 qed "Ord_cardinal"; |
227 |
227 |