tuned document;
authorwenzelm
Fri, 25 Jan 2008 23:05:23 +0100
changeset 25972 94b15338da8d
parent 25971 21953dda56ee
child 25973 4a584b094aba
tuned document;
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/ParRed.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)"
--- 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]
 
--- 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"