src/HOL/Quotient.thy
changeset 45961 5cefe17916a6
parent 45802 b16f976db515
child 46468 4db76d47b51a
     1.1 --- a/src/HOL/Quotient.thy	Sat Dec 24 15:53:07 2011 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Sat Dec 24 15:53:08 2011 +0100
     1.3 @@ -15,6 +15,13 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 +  An aside: contravariant functorial structure of sets.
     1.8 +*}
     1.9 +
    1.10 +enriched_type vimage
    1.11 +  by (simp_all add: fun_eq_iff vimage_compose)
    1.12 +
    1.13 +text {*
    1.14    Basic definition for equivalence relations
    1.15    that are represented by predicates.
    1.16  *}