src/HOL/Quotient.thy
changeset 47488 be6dd389639d
parent 47436 d8fad618a67a
child 47544 e455cdaac479
     1.1 --- a/src/HOL/Quotient.thy	Sun Apr 15 20:41:46 2012 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Sun Apr 15 20:51:07 2012 +0200
     1.3 @@ -19,13 +19,6 @@
     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  *}
    1.17 @@ -911,3 +904,4 @@
    1.18    fun_rel (infixr "===>" 55)
    1.19  
    1.20  end
    1.21 +