src/ZF/OrdQuant.thy
 changeset 12820 02e2ff3e4d37 parent 12763 6cecd9dfd53f child 12825 f1f7964ed05c
```     1.1 --- a/src/ZF/OrdQuant.thy	Mon Jan 21 10:52:05 2002 +0100
1.2 +++ b/src/ZF/OrdQuant.thy	Mon Jan 21 11:25:45 2002 +0100
1.3 @@ -45,8 +45,7 @@
1.4  lemma Union_upper_le:
1.5       "\<lbrakk>j: J;  i\<le>j;  Ord(\<Union>(J))\<rbrakk> \<Longrightarrow> i \<le> \<Union>J"
1.6  apply (subst Union_eq_UN)
1.7 -apply (rule UN_upper_le)
1.8 -apply auto
1.9 +apply (rule UN_upper_le, auto)
1.10  done
1.11
1.12  lemma zero_not_Limit [iff]: "~ Limit(0)"
1.13 @@ -61,8 +60,7 @@
1.14  done
1.15
1.16  lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
1.17 -apply (simp add: Limit_def lt_Ord2)
1.18 -apply clarify
1.19 +apply (simp add: Limit_def lt_Ord2, clarify)
1.20  apply (drule_tac i=y in ltD)
1.21  apply (blast intro: lt_trans1 succ_leI ltI lt_Ord2)
1.22  done
1.23 @@ -115,8 +113,7 @@
1.24
1.25  lemma OUN_upper_le:
1.26       "\<lbrakk>a<A;  i\<le>b(a);  Ord(\<Union>x<A. b(x))\<rbrakk> \<Longrightarrow> i \<le> (\<Union>x<A. b(x))"
1.27 -apply (unfold OUnion_def)
1.28 -apply auto
1.29 +apply (unfold OUnion_def, auto)
1.30  apply (rule UN_upper_le )
1.31  apply (auto simp add: lt_def)
1.32  done
```