src/ZF/Ordinal.thy

 by (unfold Memrel_def, blast)
 
 lemma Memrel_1 [simp]: "Memrel(1) = 0"
 by (unfold Memrel_def, blast)
 
+lemma relation_Memrel: "relation(Memrel(A))"
+by (simp add: relation_def Memrel_def, blast)
+
 (*The membership relation (as a set) is well-founded.
   Proof idea: show A<=B by applying the foundation axiom to A-B *)
 lemma wf_Memrel: "wf(Memrel(A))"
 apply (unfold wf_def)
 apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) 

 lemma Transset_induct: 
     "[| i: k;  Transset(k);                           
         !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) |]
      ==>  P(i)"
 apply (simp add: Transset_def) 
-apply (erule wf_Memrel [THEN wf_induct2], blast)
-apply blast 
+apply (erule wf_Memrel [THEN wf_induct2], blast+)
 done
 
 (*Induction over an ordinal*)
 lemmas Ord_induct = Transset_induct [OF _ Ord_is_Transset]
 

 
 lemma zero_le_succ_iff [iff]: "0 le succ(x) <-> Ord(x)"
 by (blast intro: Ord_0_le elim: ltE)
 
 lemma subset_imp_le: "[| j<=i;  Ord(i);  Ord(j) |] ==> j le i"
-apply (rule not_lt_iff_le [THEN iffD1], assumption)
-apply assumption
+apply (rule not_lt_iff_le [THEN iffD1], assumption+)
 apply (blast elim: ltE mem_irrefl)
 done
 
 lemma le_imp_subset: "i le j ==> i<=j"
 by (blast dest: OrdmemD elim: ltE leE)