# HG changeset patch
# User blanchet
# Date 1458747439 -3600
# Node ID e3ca8dc01c4f0ef774a72b71e3e765ad8a7fe2cb
# Parent  add334b71e16016880572e6b4cf30bcb9b4b0a7f
proper sectioning

diff -r add334b71e16 -r e3ca8dc01c4f src/HOL/Library/BNF_Corec.thy
--- 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