# HG changeset patch
# User traytel
# Date 1350411075 -7200
# Node ID 946efb120c42c488aa51e71cdc5382fd06b5243c
# Parent  d9d73ebf9274738b1aedefa04d0975e4ef4c016c
tuned for document output

diff -r d9d73ebf9274 -r 946efb120c42 src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- 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"
diff -r d9d73ebf9274 -r 946efb120c42 src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy
--- 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}"
diff -r d9d73ebf9274 -r 946efb120c42 src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy
--- 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>