src/HOL/Conditionally_Complete_Lattices.thy
changeset 60758 d8d85a8172b5
parent 60615 e5fa1d5d3952
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      Author:     Luke S. Serafin, Carnegie Mellon University
     1.5  *)
     1.6  
     1.7 -section {* Conditionally-complete Lattices *}
     1.8 +section \<open>Conditionally-complete Lattices\<close>
     1.9  
    1.10  theory Conditionally_Complete_Lattices
    1.11  imports Main
    1.12 @@ -166,12 +166,12 @@
    1.13  end
    1.14  
    1.15  
    1.16 -text {*
    1.17 +text \<open>
    1.18  
    1.19  To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
    1.20  @{const Inf} in theorem names with c.
    1.21  
    1.22 -*}
    1.23 +\<close>
    1.24  
    1.25  class conditionally_complete_lattice = lattice + Sup + Inf +
    1.26    assumes cInf_lower: "x \<in> X \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> x"
    1.27 @@ -426,13 +426,13 @@
    1.28  proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
    1.29    show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
    1.30      by (rule cSup_upper, auto simp: bdd_above_def)
    1.31 -       (metis `a < b` `\<not> P b` linear less_le)
    1.32 +       (metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le)
    1.33  next
    1.34    show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
    1.35      apply (rule cSup_least) 
    1.36      apply auto
    1.37      apply (metis less_le_not_le)
    1.38 -    apply (metis `a<b` `~ P b` linear less_le)
    1.39 +    apply (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le)
    1.40      done
    1.41  next
    1.42    fix x
    1.43 @@ -447,7 +447,7 @@
    1.44      assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
    1.45      thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
    1.46        by (rule_tac cSup_upper, auto simp: bdd_above_def)
    1.47 -         (metis `a<b` `~ P b` linear less_le)
    1.48 +         (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le)
    1.49  qed
    1.50  
    1.51  end
    1.52 @@ -538,13 +538,13 @@
    1.53        { fix z assume "z \<in> X"
    1.54          have "z \<le> Max (X \<inter> {x..y})"
    1.55          proof cases
    1.56 -          assume "x \<le> z" with `z \<in> X` `X \<subseteq> {..y}` *(1) show ?thesis
    1.57 +          assume "x \<le> z" with \<open>z \<in> X\<close> \<open>X \<subseteq> {..y}\<close> *(1) show ?thesis
    1.58              by (auto intro!: Max_ge)
    1.59          next
    1.60            assume "\<not> x \<le> z"
    1.61            then have "z < x" by simp
    1.62            also have "x \<le> Max (X \<inter> {x..y})"
    1.63 -            using `x \<in> X` *(1) `x \<le> y` by (intro Max_ge) auto
    1.64 +            using \<open>x \<in> X\<close> *(1) \<open>x \<le> y\<close> by (intro Max_ge) auto
    1.65            finally show ?thesis by simp
    1.66          qed }
    1.67        note le = this