src/HOL/Library/Quotient.thy
changeset 21404 eb85850d3eb7
parent 19086 1b3780be6cc2
child 22390 378f34b1e380
     1.1 --- a/src/HOL/Library/Quotient.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4  *}
     1.5  
     1.6  definition
     1.7 -  "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
     1.8 +  "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
     1.9    "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
    1.10  
    1.11  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
    1.12 @@ -134,7 +134,7 @@
    1.13  subsection {* Picking representing elements *}
    1.14  
    1.15  definition
    1.16 -  pick :: "'a::equiv quot => 'a"
    1.17 +  pick :: "'a::equiv quot => 'a" where
    1.18    "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
    1.19  
    1.20  theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"