src/HOL/Library/Order_Continuity.thy
changeset 60500 903bb1495239
parent 60427 b4b672f09270
child 60614 e39e6881985c
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     David von Oheimb, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Continuity and iterations (of set transformers) *}
     1.8 +section \<open>Continuity and iterations (of set transformers)\<close>
     1.9  
    1.10  theory Order_Continuity
    1.11  imports Main
    1.12 @@ -34,7 +34,7 @@
    1.13    and have the advantage that these names are duals.
    1.14  \<close>
    1.15  
    1.16 -subsection {* Continuity for complete lattices *}
    1.17 +subsection \<open>Continuity for complete lattices\<close>
    1.18  
    1.19  definition
    1.20    sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.21 @@ -59,7 +59,7 @@
    1.22  lemma sup_continuous_lfp:
    1.23    assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    1.24  proof (rule antisym)
    1.25 -  note mono = sup_continuous_mono[OF `sup_continuous F`]
    1.26 +  note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>]
    1.27    show "?U \<le> lfp F"
    1.28    proof (rule SUP_least)
    1.29      fix i show "(F ^^ i) bot \<le> lfp F"
    1.30 @@ -84,7 +84,7 @@
    1.31        thus ?thesis by (auto simp add: mono_iff_le_Suc)
    1.32      qed
    1.33      hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
    1.34 -      using `sup_continuous F` by (simp add: sup_continuous_def)
    1.35 +      using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def)
    1.36      also have "\<dots> \<le> ?U"
    1.37        by (fast intro: SUP_least SUP_upper)
    1.38      finally show "F ?U \<le> ?U" .
    1.39 @@ -127,7 +127,7 @@
    1.40  lemma inf_continuous_gfp:
    1.41    assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
    1.42  proof (rule antisym)
    1.43 -  note mono = inf_continuous_mono[OF `inf_continuous F`]
    1.44 +  note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>]
    1.45    show "gfp F \<le> ?U"
    1.46    proof (rule INF_greatest)
    1.47      fix i show "gfp F \<le> (F ^^ i) top"
    1.48 @@ -154,7 +154,7 @@
    1.49      have "?U \<le> (INF i. (F ^^ Suc i) top)"
    1.50        by (fast intro: INF_greatest INF_lower)
    1.51      also have "\<dots> \<le> F ?U"
    1.52 -      by (simp add: inf_continuousD `inf_continuous F` *)
    1.53 +      by (simp add: inf_continuousD \<open>inf_continuous F\<close> *)
    1.54      finally show "?U \<le> F ?U" .
    1.55    qed
    1.56  qed