src/HOL/Library/Quotient.thy

  \medskip Abstracted equivalence classes are the canonical
  representation of elements of a quotient type.
 *}
 
 definition
-  "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
+  "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
   "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
 
 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
   fix R assume R: "A = Abs_quot R"

 
 
 subsection {* Picking representing elements *}
 
 definition
-  pick :: "'a::equiv quot => 'a"
+  pick :: "'a::equiv quot => 'a" where
   "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
 
 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
 proof (unfold pick_def)
   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"