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
```