changeset 782 | 200a16083201 |
parent 765 | 06a484afc603 |
child 792 | 5d2a7634da46 |
--- a/src/ZF/Cardinal.ML Wed Dec 14 10:26:30 1994 +0100 +++ b/src/ZF/Cardinal.ML Wed Dec 14 11:41:49 1994 +0100 @@ -219,7 +219,7 @@ goal Cardinal.thy "!!K. Card(K) ==> K le |K|"; by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); -val Card_cardinal_le = result(); +qed "Card_cardinal_le"; goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; by (rtac Ord_Least 1);