src/ZF/Ordinal.thy
changeset 13269 3ba9be497c33
parent 13243 ba53d07d32d5
child 13356 c9cfe1638bf2
     1.1 --- a/src/ZF/Ordinal.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -290,6 +290,9 @@
     1.4  lemma Memrel_1 [simp]: "Memrel(1) = 0"
     1.5  by (unfold Memrel_def, blast)
     1.6  
     1.7 +lemma relation_Memrel: "relation(Memrel(A))"
     1.8 +by (simp add: relation_def Memrel_def, blast)
     1.9 +
    1.10  (*The membership relation (as a set) is well-founded.
    1.11    Proof idea: show A<=B by applying the foundation axiom to A-B *)
    1.12  lemma wf_Memrel: "wf(Memrel(A))"
    1.13 @@ -316,8 +319,7 @@
    1.14          !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) |]
    1.15       ==>  P(i)"
    1.16  apply (simp add: Transset_def) 
    1.17 -apply (erule wf_Memrel [THEN wf_induct2], blast)
    1.18 -apply blast 
    1.19 +apply (erule wf_Memrel [THEN wf_induct2], blast+)
    1.20  done
    1.21  
    1.22  (*Induction over an ordinal*)
    1.23 @@ -404,8 +406,7 @@
    1.24  by (blast intro: Ord_0_le elim: ltE)
    1.25  
    1.26  lemma subset_imp_le: "[| j<=i;  Ord(i);  Ord(j) |] ==> j le i"
    1.27 -apply (rule not_lt_iff_le [THEN iffD1], assumption)
    1.28 -apply assumption
    1.29 +apply (rule not_lt_iff_le [THEN iffD1], assumption+)
    1.30  apply (blast elim: ltE mem_irrefl)
    1.31  done
    1.32