src/HOL/Library/Quotient.thy
changeset 18551 be0705186ff5
parent 18372 2bffdf62fe7f
child 18730 843da46f89ac
     1.1 --- a/src/HOL/Library/Quotient.thy	Tue Jan 03 11:32:16 2006 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Tue Jan 03 11:32:55 2006 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4  *}
     1.5  
     1.6  constdefs
     1.7 -  class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
     1.8 +  "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
     1.9    "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
    1.10  
    1.11  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"