--- a/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy Tue Oct 16 18:50:53 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy Tue Oct 16 20:11:15 2012 +0200
@@ -20,7 +20,7 @@
Nplus_comm: "(a::N) + b = b + (a::N)"
and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
-section{* Parallel composition *}
+subsection{* Corecursive Definition of Parallel Composition *}
fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
fun par_c where
@@ -30,7 +30,6 @@
declare par_r.simps[simp del] declare par_c.simps[simp del]
-(* Corecursive definition of parallel composition: *)
definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where
"par \<equiv> unfold par_r par_c"
@@ -67,7 +66,7 @@
using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto
-section{* Structural coinductive proofs *}
+subsection{* Structural Coinduction Proofs *}
lemma set_rel_sum_rel_eq[simp]:
"set_rel (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>