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