src/ZF/Cardinal.ML
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);