--- a/src/HOL/Library/Quotient_Set.thy Thu Apr 26 01:05:06 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Thu Apr 26 12:01:58 2012 +0200
@@ -185,7 +185,7 @@
subsection {* Setup for lifting package *}
-lemma Quotient_set:
+lemma Quotient_set[quot_map]:
assumes "Quotient R Abs Rep T"
shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
using assms unfolding Quotient_alt_def4
@@ -193,8 +193,6 @@
apply (simp add: set_rel_def, fast)
done
-declare [[map set = (set_rel, Quotient_set)]]
-
lemma set_invariant_commute [invariant_commute]:
"set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast