src/HOL/Library/Quotient_List.thy
changeset 47777 f29e7dcd7c40
parent 47660 7a5c681c0265
child 47923 ba9df9685e7c
--- 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)