src/HOL/SupInf.thy
changeset 33657 a4179bf442d1
parent 33609 059cd49e4b1e
child 35028 108662d50512
     1.1 --- a/src/HOL/SupInf.thy	Thu Nov 12 14:32:21 2009 -0800
     1.2 +++ b/src/HOL/SupInf.thy	Fri Nov 13 14:14:04 2009 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4    shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
     1.5          \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
     1.6    by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
     1.7 -        insert_not_empty real_le_anti_sym)
     1.8 +        insert_not_empty real_le_antisym)
     1.9  
    1.10  lemma Sup_le:
    1.11    fixes S :: "real set"
    1.12 @@ -317,7 +317,7 @@
    1.13    fixes a :: real
    1.14    shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
    1.15    by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
    1.16 -        insert_absorb insert_not_empty real_le_anti_sym)
    1.17 +        insert_absorb insert_not_empty real_le_antisym)
    1.18  
    1.19  lemma Inf_ge: 
    1.20    fixes S :: "real set"
    1.21 @@ -397,7 +397,7 @@
    1.22    fixes S :: "real set"
    1.23    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
    1.24  by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
    1.25 -          real_le_anti_sym real_le_linear)
    1.26 +          real_le_antisym real_le_linear)
    1.27  
    1.28  lemma Inf_finite_gt_iff: 
    1.29    fixes S :: "real set"