src/HOL/Library/Quotient.thy
changeset 10392 f27afee8475d
parent 10390 1d54567bed24
child 10437 7528f9e30ca4
equal deleted inserted replaced
10391:0025fd11882c 10392:f27afee8475d
    34 text {*
    34 text {*
    35  \medskip The quotient type @{text "'a quot"} consists of all
    35  \medskip The quotient type @{text "'a quot"} consists of all
    36  \emph{equivalence classes} over elements of the base type @{typ 'a}.
    36  \emph{equivalence classes} over elements of the base type @{typ 'a}.
    37 *}
    37 *}
    38 
    38 
    39 typedef 'a quot = "{{x. a \<sim> x}| a::'a::eqv. True}"
    39 typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
    40   by blast
    40   by blast
    41 
    41 
    42 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    42 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    43   by (unfold quot_def) blast
    43   by (unfold quot_def) blast
    44 
    44