src/HOL/Library/Quotient_Type.thy
changeset 69593 3dda49e08b9d
parent 61585 a9599d3d7610
     1.1 --- a/src/HOL/Library/Quotient_Type.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Type.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4  end
     1.5  
     1.6  text \<open>The quotient type \<open>'a quot\<close> consists of all \emph{equivalence
     1.7 -  classes} over elements of the base type @{typ 'a}.\<close>
     1.8 +  classes} over elements of the base type \<^typ>\<open>'a\<close>.\<close>
     1.9  
    1.10  definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
    1.11