--- 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"