1.1 --- a/src/HOL/Library/Quotient_List.thy	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Wed May 16 19:15:45 2012 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4      by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
     1.5  qed
     1.6  
     1.7 -lemma list_reflp:
     1.8 +lemma list_reflp[reflp_preserve]:
     1.9    assumes "reflp R"
    1.10    shows "reflp (list_all2 R)"
    1.11  proof (rule reflpI)