src/ZF/CardinalArith.thy

 apply (unfold csucc_def)
 apply (rule LeastI)
 apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+
 done
 
-lemmas Card_csucc = csucc_basic [THEN conjunct1, standard]
-
-lemmas lt_csucc = csucc_basic [THEN conjunct2, standard]
+lemmas Card_csucc = csucc_basic [THEN conjunct1]
+
+lemmas lt_csucc = csucc_basic [THEN conjunct2]
 
 lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)"
 by (blast intro: Ord_0_le lt_csucc lt_trans1)
 
 lemma csucc_le: "[| Card(L);  K<L |] ==> csucc(K) le L"

 done
 
 
 subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*}
 
-lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard]
+lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel]
 
 lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n"
 apply (rule eqpoll_trans)
 apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
 apply (erule nat_implies_well_ord)+