src/HOL/Inductive.thy
 changeset 61799 4cf66f21b764 parent 61337 4645502c3c64 child 61952 546958347e05
```     1.1 --- a/src/HOL/Inductive.thy	Mon Dec 07 10:23:50 2015 +0100
1.2 +++ b/src/HOL/Inductive.thy	Mon Dec 07 10:38:04 2015 +0100
1.3 @@ -21,11 +21,11 @@
1.4
1.5  definition
1.6    lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.7 -  "lfp f = Inf {u. f u \<le> u}"    --\<open>least fixed point\<close>
1.8 +  "lfp f = Inf {u. f u \<le> u}"    \<comment>\<open>least fixed point\<close>
1.9
1.10  definition
1.11    gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.12 -  "gfp f = Sup {u. u \<le> f u}"    --\<open>greatest fixed point\<close>
1.13 +  "gfp f = Sup {u. u \<le> f u}"    \<comment>\<open>greatest fixed point\<close>
1.14
1.15
1.16  subsection\<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
1.17 @@ -101,7 +101,7 @@
1.18    using assms by (rule lfp_ordinal_induct)
1.19
1.20
1.21 -text\<open>Definition forms of @{text lfp_unfold} and @{text lfp_induct},
1.22 +text\<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>,
1.23      to control unfolding\<close>
1.24
1.25  lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
1.26 @@ -230,7 +230,7 @@
1.27  apply (simp_all)
1.28  done
1.29
1.30 -text\<open>Definition forms of @{text gfp_unfold} and @{text coinduct},
1.31 +text\<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>,
1.32      to control unfolding\<close>
1.33
1.34  lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
```