src/HOL/Lambda/Commutation.thy
changeset 25972 94b15338da8d
parent 23815 73dbab55d283
child 28455 a79701b14a30
     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)"