# HG changeset patch
# User lcp
# Date 787596109 -3600
# Node ID 23f55b829ccb38b74b2a91a356582fcc4e909679
# Parent  13aa1e3d8a3a1b77857a5dee22f8d3026a27c214
Limit_csucc: moved to InfDatatype and proved explicitly in
theory InfDatatype.thy

diff -r 13aa1e3d8a3a -r 23f55b829ccb src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Fri Dec 16 17:39:43 1994 +0100
+++ b/src/ZF/CardinalArith.ML	Fri Dec 16 17:41:49 1994 +0100
@@ -439,8 +439,9 @@
 by (safe_tac (ZF_cs addSEs [mem_irrefl] 
                     addSIs [Un_upper1_le, Un_upper2_le]));
 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [lt_def, succI2, Ord_succ])));
-qed "csquareD_lemma";
-val csquareD = csquareD_lemma RS mp |> standard;
+val csquareD_lemma = result();
+
+bind_thm ("csquareD", csquareD_lemma RS mp);
 
 goalw CardinalArith.thy [pred_def]
  "!!K. z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
@@ -709,9 +710,9 @@
 		      Ord_jump_cardinal] 1));
 qed "csucc_basic";
 
-val Card_csucc = csucc_basic RS conjunct1 |> standard;
+bind_thm ("Card_csucc", csucc_basic RS conjunct1);
 
-val lt_csucc = csucc_basic RS conjunct2 |> standard;
+bind_thm ("lt_csucc", csucc_basic RS conjunct2);
 
 goal CardinalArith.thy "!!K. Ord(K) ==> 0 < csucc(K)";
 by (resolve_tac [[Ord_0_le, lt_csucc] MRS lt_trans1] 1);
@@ -750,4 +751,3 @@
 				  lt_csucc RS leI RSN (2,le_trans)]) 1);
 qed "InfCard_csucc";
 
-val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard;