tuned document;
authorwenzelm
Fri Jan 25 23:05:23 2008 +0100 (2008-01-25)
changeset 2597294b15338da8d
parent 25971 21953dda56ee
child 25973 4a584b094aba
tuned document;
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/ParRed.thy
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Fri Jan 25 22:04:46 2008 +0100
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Jan 25 23:05:23 2008 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  subsection {* Basic lemmas *}
     1.6  
     1.7 -subsubsection {* square *}
     1.8 +subsubsection {* @{text "square"} *}
     1.9  
    1.10  lemma square_sym: "square R S T U ==> square S R U T"
    1.11    apply (unfold square_def)
    1.12 @@ -70,7 +70,7 @@
    1.13    done
    1.14  
    1.15  
    1.16 -subsubsection {* commute *}
    1.17 +subsubsection {* @{text "commute"} *}
    1.18  
    1.19  lemma commute_sym: "commute R S ==> commute S R"
    1.20    apply (unfold commute_def)
    1.21 @@ -89,7 +89,7 @@
    1.22    done
    1.23  
    1.24  
    1.25 -subsubsection {* diamond, confluence, and union *}
    1.26 +subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *}
    1.27  
    1.28  lemma diamond_Un:
    1.29      "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
     2.1 --- a/src/HOL/Lambda/InductTermi.thy	Fri Jan 25 22:04:46 2008 +0100
     2.2 +++ b/src/HOL/Lambda/InductTermi.thy	Fri Jan 25 23:05:23 2008 +0100
     2.3 @@ -21,7 +21,7 @@
     2.4    | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
     2.5  
     2.6  
     2.7 -subsection {* Every term in IT terminates *}
     2.8 +subsection {* Every term in @{text "IT"} terminates *}
     2.9  
    2.10  lemma double_induction_lemma [rule_format]:
    2.11    "termip beta s ==> \<forall>t. termip beta t -->
    2.12 @@ -56,7 +56,7 @@
    2.13    done
    2.14  
    2.15  
    2.16 -subsection {* Every terminating term is in IT *}
    2.17 +subsection {* Every terminating term is in @{text "IT"} *}
    2.18  
    2.19  declare Var_apps_neq_Abs_apps [symmetric, simp]
    2.20  
     3.1 --- a/src/HOL/Lambda/ParRed.thy	Fri Jan 25 22:04:46 2008 +0100
     3.2 +++ b/src/HOL/Lambda/ParRed.thy	Fri Jan 25 23:05:23 2008 +0100
     3.3 @@ -55,7 +55,7 @@
     3.4    done
     3.5  
     3.6  
     3.7 -subsection {* Misc properties of par-beta *}
     3.8 +subsection {* Misc properties of @{text "par_beta"} *}
     3.9  
    3.10  lemma par_beta_lift [simp]:
    3.11      "t => t' \<Longrightarrow> lift t n => lift t' n"