src/HOL/Library/Quotient.thy
changeset 19086 1b3780be6cc2
parent 18730 843da46f89ac
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Library/Quotient.thy	Thu Feb 16 21:11:58 2006 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Thu Feb 16 21:12:00 2006 +0100
     1.3 @@ -74,9 +74,9 @@
     1.4   representation of elements of a quotient type.
     1.5  *}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
    1.10 -  "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
    1.11 +  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
    1.12  
    1.13  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
    1.14  proof (cases A)
    1.15 @@ -133,9 +133,9 @@
    1.16  
    1.17  subsection {* Picking representing elements *}
    1.18  
    1.19 -constdefs
    1.20 +definition
    1.21    pick :: "'a::equiv quot => 'a"
    1.22 -  "pick A == SOME a. A = \<lfloor>a\<rfloor>"
    1.23 +  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
    1.24  
    1.25  theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
    1.26  proof (unfold pick_def)