src/HOL/Conditionally_Complete_Lattices.thy
changeset 67091 1393c2340eec
parent 65466 b0f89998c2a1
child 67458 e090941f9f42
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Apr 12 09:27:47 2017 +0200
     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