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)"