src/HOL/Conditionally_Complete_Lattices.thy
 changeset 67091 1393c2340eec parent 65466 b0f89998c2a1 child 67458 e090941f9f42
```     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -430,7 +430,7 @@
1.4    assumes "a < b" and "P a" and "\<not> P b"
1.5    shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
1.6               (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
1.7 -proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
1.8 +proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x}"], auto)
1.9    show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
1.10      by (rule cSup_upper, auto simp: bdd_above_def)
1.11         (metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le)
1.12 @@ -439,7 +439,7 @@
1.13      apply (rule cSup_least)
1.14      apply auto
1.15      apply (metis less_le_not_le)
1.16 -    apply (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le)
1.17 +    apply (metis \<open>a<b\<close> \<open>\<not> P b\<close> linear less_le)
1.18      done
1.19  next
1.20    fix x
1.21 @@ -454,7 +454,7 @@
1.22      assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
1.23      thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
1.24        by (rule_tac cSup_upper, auto simp: bdd_above_def)
1.25 -         (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le)
1.26 +         (metis \<open>a<b\<close> \<open>\<not> P b\<close> linear less_le)
1.27  qed
1.28
1.29  end
```