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.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
```