diff -r 2b1d3eda59eb -r 091bcd569441 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Fri Apr 20 18:29:21 2012 +0200
@@ -207,6 +207,8 @@
   shows "list_all2 R x x"
   by (induct x) (auto simp add: a)
 
+subsection {* Setup for lifting package *}
+
 lemma list_quotient:
   assumes "Quotient R Abs Rep T"
   shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)"
@@ -251,4 +253,13 @@
 
 declare [[map list = (list_all2, list_quotient)]]
 
+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) 
+  apply (intro allI) 
+  apply (induct_tac rule: list_induct2') 
+  apply simp_all 
+  apply metis
+done
+
 end