--- a/src/HOL/Library/Quotient_List.thy Thu Apr 26 01:05:06 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy Thu Apr 26 12:01:58 2012 +0200
@@ -178,7 +178,7 @@
subsection {* Setup for lifting package *}
-lemma Quotient_list:
+lemma Quotient_list[quot_map]:
assumes "Quotient R Abs Rep T"
shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
proof (unfold Quotient_alt_def, intro conjI allI impI)
@@ -199,8 +199,6 @@
by (induct xs ys rule: list_induct2', simp_all, metis 3)
qed
-declare [[map list = (list_all2, Quotient_list)]]
-
lemma list_invariant_commute [invariant_commute]:
"list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def)