src/HOL/Conditionally_Complete_Lattices.thy
changeset 61824 dcbe9f756ae0
parent 61169 4de9ff3ea29a
child 62343 24106dc44def
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Dec 07 10:49:08 2015 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Thu Dec 10 13:38:40 2015 +0000
     1.3 @@ -413,11 +413,11 @@
     1.4  
     1.5  lemma less_cSupD:
     1.6    "X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
     1.7 -  by (metis less_cSup_iff not_leE bdd_above_def)
     1.8 +  by (metis less_cSup_iff not_le_imp_less bdd_above_def)
     1.9  
    1.10  lemma cInf_lessD:
    1.11    "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
    1.12 -  by (metis cInf_less_iff not_leE bdd_below_def)
    1.13 +  by (metis cInf_less_iff not_le_imp_less bdd_below_def)
    1.14  
    1.15  lemma complete_interval:
    1.16    assumes "a < b" and "P a" and "\<not> P b"