--- a/src/HOL/Library/BNF_Corec.thy Wed Mar 23 16:37:13 2016 +0100
+++ b/src/HOL/Library/BNF_Corec.thy Wed Mar 23 16:37:19 2016 +0100
@@ -7,7 +7,7 @@
Generalized corecursor sugar ("corec" and friends).
*)
-chapter {* Generalized Corecursor Sugar (corec and friends) *}
+section \<open>Generalized Corecursor Sugar (corec and friends)\<close>
theory BNF_Corec
imports Main
@@ -61,7 +61,7 @@
by simp
-section \<open>Coinduction\<close>
+subsection \<open>Coinduction\<close>
lemma eq_comp_compI: "a o b = f o x \<Longrightarrow> x o c = id \<Longrightarrow> f = a o (b o c)"
unfolding fun_eq_iff by simp