src/HOLCF/Representable.thy
changeset 35900 aa5dfb03eb1e
parent 35652 05ca920cd94b
child 35901 12f09bf2c77f
     1.1 --- a/src/HOLCF/Representable.thy	Mon Mar 22 19:29:11 2010 +0100
     1.2 +++ b/src/HOLCF/Representable.thy	Mon Mar 22 12:52:51 2010 -0700
     1.3 @@ -35,7 +35,7 @@
     1.4  lemmas prj_strict = rep.p_strict
     1.5  
     1.6  
     1.7 -subsection {* Making @{term rep} the default class *}
     1.8 +subsection {* Making \emph{rep} the default class *}
     1.9  
    1.10  text {*
    1.11    From now on, free type variables are assumed to be in class
    1.12 @@ -342,7 +342,7 @@
    1.13  use "Tools/repdef.ML"
    1.14  
    1.15  
    1.16 -subsection {* Instances of class @{text rep} *}
    1.17 +subsection {* Instances of class \emph{rep} *}
    1.18  
    1.19  subsubsection {* Universal Domain *}
    1.20