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