--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Tue Oct 16 18:50:53 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Tue Oct 16 20:11:15 2012 +0200
@@ -18,8 +18,7 @@
codata dtree = NNode (root: N) (ccont: "(T + dtree) fset")
-
-subsection{* The characteristic lemmas transported from fset to set *}
+subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *}
definition "Node n as \<equiv> NNode n (the_inv fset as)"
definition "cont \<equiv> fset o ccont"
--- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy Tue Oct 16 18:50:53 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy Tue Oct 16 20:11:15 2012 +0200
@@ -21,7 +21,7 @@
and used: "\<And> n. \<exists> tns. (n,tns) \<in> P"
-subsection{* Tree basics: frontier, interior, etc. *}
+subsection{* Tree Basics: frontier, interior, etc. *}
(* Frontier *)
@@ -309,7 +309,7 @@
by (metis inItr.Base subtr_inItr subtr_rootL_in)
-subsection{* The immediate subtree function *}
+subsection{* The Immediate Subtree Function *}
(* production of: *)
abbreviation "prodOf tr \<equiv> (id \<oplus> root) ` (cont tr)"
@@ -343,7 +343,7 @@
by (metis (lifting) assms image_iff sum_map.simps(2))
-subsection{* Well-formed derivation trees *}
+subsection{* Well-Formed Derivation Trees *}
hide_const wf
@@ -448,7 +448,7 @@
qed
-subsection{* Default trees *}
+subsection{* Default Trees *}
(* Pick a left-hand side of a production for each nonterminal *)
definition S where "S n \<equiv> SOME tns. (n,tns) \<in> P"
@@ -488,7 +488,7 @@
qed
-subsection{* Hereditary substitution *}
+subsection{* Hereditary Substitution *}
(* Auxiliary concept: The root-ommiting frontier: *)
definition "inFrr ns tr t \<equiv> \<exists> tr'. Inr tr' \<in> cont tr \<and> inFr ns tr' t"
@@ -679,7 +679,7 @@
end (* context *)
-subsection{* Regular trees *}
+subsection{* Regular Trees *}
hide_const regular
@@ -771,7 +771,7 @@
-subsection {* Paths in a regular tree *}
+subsection {* Paths in a Regular Tree *}
inductive path :: "(N \<Rightarrow> dtree) \<Rightarrow> N list \<Rightarrow> bool" for f where
Base: "path f [n]"
@@ -915,7 +915,7 @@
-subsection{* The regular cut of a tree *}
+subsection{* The Regular Cut of a Tree *}
context fixes tr0 :: dtree
begin
@@ -1082,7 +1082,7 @@
end (* context *)
-subsection{* Recursive description of the regular tree frontiers *}
+subsection{* Recursive Description of the Regular Tree Frontiers *}
lemma regular_inFr:
assumes r: "regular tr" and In: "root tr \<in> ns"
@@ -1131,7 +1131,7 @@
by (simp, metis (lifting) inFr_Ind_minus insert_Diff)
-subsection{* The generated languages *}
+subsection{* The Generated Languages *}
(* The (possibly inifinite tree) generated language *)
definition "L ns n \<equiv> {Fr ns tr | tr. wf tr \<and> root tr = n}"
--- 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>