src/HOL/Quotient.thy
changeset 47579 28f6f4ad69bf
parent 47544 e455cdaac479
child 47626 f7b1034cb9ce
     1.1 --- a/src/HOL/Quotient.thy	Thu Apr 19 11:10:03 2012 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Thu Apr 19 10:49:47 2012 +0200
     1.3 @@ -38,10 +38,6 @@
     1.4  
     1.5  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     1.6  
     1.7 -lemma vimage_id:
     1.8 -  "vimage id = id"
     1.9 -  unfolding vimage_def fun_eq_iff by auto
    1.10 -
    1.11  lemma set_rel_eq:
    1.12    "set_rel op = = op ="
    1.13    by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)