# HG changeset patch
# User wenzelm
# Date 1201298723 -3600
# Node ID 94b15338da8d2fec09a3cd9aea269ff0c168ddb4
# Parent  21953dda56ee30744ef7556c011e4f6b916058c5
tuned document;

diff -r 21953dda56ee -r 94b15338da8d src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Fri Jan 25 22:04:46 2008 +0100
+++ b/src/HOL/Lambda/Commutation.thy	Fri Jan 25 23:05:23 2008 +0100
@@ -35,7 +35,7 @@
 
 subsection {* Basic lemmas *}
 
-subsubsection {* square *}
+subsubsection {* @{text "square"} *}
 
 lemma square_sym: "square R S T U ==> square S R U T"
   apply (unfold square_def)
@@ -70,7 +70,7 @@
   done
 
 
-subsubsection {* commute *}
+subsubsection {* @{text "commute"} *}
 
 lemma commute_sym: "commute R S ==> commute S R"
   apply (unfold commute_def)
@@ -89,7 +89,7 @@
   done
 
 
-subsubsection {* diamond, confluence, and union *}
+subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *}
 
 lemma diamond_Un:
     "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
diff -r 21953dda56ee -r 94b15338da8d src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Fri Jan 25 22:04:46 2008 +0100
+++ b/src/HOL/Lambda/InductTermi.thy	Fri Jan 25 23:05:23 2008 +0100
@@ -21,7 +21,7 @@
   | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
 
 
-subsection {* Every term in IT terminates *}
+subsection {* Every term in @{text "IT"} terminates *}
 
 lemma double_induction_lemma [rule_format]:
   "termip beta s ==> \<forall>t. termip beta t -->
@@ -56,7 +56,7 @@
   done
 
 
-subsection {* Every terminating term is in IT *}
+subsection {* Every terminating term is in @{text "IT"} *}
 
 declare Var_apps_neq_Abs_apps [symmetric, simp]
 
diff -r 21953dda56ee -r 94b15338da8d src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Fri Jan 25 22:04:46 2008 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Fri Jan 25 23:05:23 2008 +0100
@@ -55,7 +55,7 @@
   done
 
 
-subsection {* Misc properties of par-beta *}
+subsection {* Misc properties of @{text "par_beta"} *}
 
 lemma par_beta_lift [simp]:
     "t => t' \<Longrightarrow> lift t n => lift t' n"