src/HOL/Library/BNF_Corec.thy
changeset 62700 e3ca8dc01c4f
parent 62692 0701f25fac39
child 64378 e9eb0b99a44c
     1.1 --- a/src/HOL/Library/BNF_Corec.thy	Wed Mar 23 16:37:13 2016 +0100
     1.2 +++ b/src/HOL/Library/BNF_Corec.thy	Wed Mar 23 16:37:19 2016 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  Generalized corecursor sugar ("corec" and friends).
     1.5  *)
     1.6  
     1.7 -chapter {* Generalized Corecursor Sugar (corec and friends) *}
     1.8 +section \<open>Generalized Corecursor Sugar (corec and friends)\<close>
     1.9  
    1.10  theory BNF_Corec
    1.11  imports Main
    1.12 @@ -61,7 +61,7 @@
    1.13    by simp
    1.14  
    1.15  
    1.16 -section \<open>Coinduction\<close>
    1.17 +subsection \<open>Coinduction\<close>
    1.18  
    1.19  lemma eq_comp_compI: "a o b = f o x \<Longrightarrow> x o c = id \<Longrightarrow> f = a o (b o c)"
    1.20    unfolding fun_eq_iff by simp