src/HOL/BNF_Greatest_Fixpoint.thy
changeset 60758 d8d85a8172b5
parent 58889 5b7a9633cfa8
child 61032 b57df8eecad6
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  Greatest fixpoint (codatatype) operation on bounded natural functors.
     1.5  *)
     1.6  
     1.7 -section {* Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors *}
     1.8 +section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close>
     1.9  
    1.10  theory BNF_Greatest_Fixpoint
    1.11  imports BNF_Fixpoint_Base String
    1.12 @@ -17,7 +17,7 @@
    1.13    "primcorec" :: thy_decl
    1.14  begin
    1.15  
    1.16 -setup {* Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj} *}
    1.17 +setup \<open>Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\<close>
    1.18  
    1.19  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.20    by simp
    1.21 @@ -240,7 +240,7 @@
    1.22    unfolding rel_fun_def image2p_def by auto
    1.23  
    1.24  
    1.25 -subsection {* Equivalence relations, quotients, and Hilbert's choice *}
    1.26 +subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
    1.27  
    1.28  lemma equiv_Eps_in:
    1.29  "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"