--- a/Nominal/Ex/Lambda.thy	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 16 20:07:03 2011 +0100
@@ -10,7 +10,8 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
-text {* free name function *}
+
+section {* free name function *}
 
 text {* first returns an atom list *}
 
@@ -20,7 +21,8 @@
   "frees_lst (Var x) = [atom x]"
 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
-  unfolding eqvt_def frees_lst_graph_def
+  unfolding eqvt_def
+  unfolding frees_lst_graph_def
   apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
@@ -74,7 +76,9 @@
   by (metis fresh_fun_app)
 
 
-text {* A test with a locale and an interpretation. *}
+section {* A test with a locale and an interpretation. *}
+
+text {* conclusion: it is no necessary *}
 
 locale test =
    fixes f1::"name \<Rightarrow> ('a::pt)"
@@ -126,7 +130,7 @@
   apply (simp_all add: eqvt_def permute_fun_def permute_pure)
   done
 
-text {* height function *}
+section {* height function *}
 
 nominal_primrec
   height :: "lam \<Rightarrow> int"
@@ -149,7 +153,7 @@
 thm height.simps
 
   
-text {* capture - avoiding substitution *}
+section {* capture-avoiding substitution *}
 
 nominal_primrec
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)