src/HOL/Library/Lattice_Constructions.thy
changeset 60500 903bb1495239
parent 58310 91ea607a34d8
child 60508 2127bee2069a
     1.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -subsection {* Values extended by a bottom element *}
     1.8 +subsection \<open>Values extended by a bottom element\<close>
     1.9  
    1.10  datatype 'a bot = Value 'a | Bot
    1.11  
    1.12 @@ -106,7 +106,7 @@
    1.13  instance bot :: (lattice) bounded_lattice_bot
    1.14  by(intro_classes)(simp add: bot_bot_def)
    1.15  
    1.16 -section {* Values extended by a top element *}
    1.17 +section \<open>Values extended by a top element\<close>
    1.18  
    1.19  datatype 'a top = Value 'a | Top
    1.20  
    1.21 @@ -205,7 +205,7 @@
    1.22  instance top :: (lattice) bounded_lattice_top
    1.23  by(intro_classes)(simp add: top_top_def)
    1.24  
    1.25 -subsection {* Values extended by a top and a bottom element *}
    1.26 +subsection \<open>Values extended by a top and a bottom element\<close>
    1.27  
    1.28  datatype 'a flat_complete_lattice = Value 'a | Bot | Top
    1.29  
    1.30 @@ -296,12 +296,12 @@
    1.31      from this have "(THE v. A - {Top} = {Value v}) = v"
    1.32        by (auto intro!: the1_equality)
    1.33      moreover
    1.34 -    from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
    1.35 +    from \<open>x : A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
    1.36        by auto
    1.37      ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
    1.38        by auto
    1.39    }
    1.40 -  from `x : A` this show "Inf A <= x"
    1.41 +  from \<open>x : A\<close> this show "Inf A <= x"
    1.42      unfolding Inf_flat_complete_lattice_def
    1.43      by fastforce
    1.44  next
    1.45 @@ -355,12 +355,12 @@
    1.46      from this have "(THE v. A - {Bot} = {Value v}) = v"
    1.47        by (auto intro!: the1_equality)
    1.48      moreover
    1.49 -    from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
    1.50 +    from \<open>x : A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
    1.51        by auto
    1.52      ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
    1.53        by auto
    1.54    }
    1.55 -  from `x : A` this show "x <= Sup A"
    1.56 +  from \<open>x : A\<close> this show "x <= Sup A"
    1.57      unfolding Sup_flat_complete_lattice_def
    1.58      by fastforce
    1.59  next