# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262879498 -3600
# Node ID ae3ed7a68e8031b825e1ba537acdc73a2297882a
# Parent  5527430f9b6fd797d99948bbce476a1d132e3c7a
Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.

diff -r 5527430f9b6f -r ae3ed7a68e80 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 16:06:13 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 16:51:38 2010 +0100
@@ -272,7 +272,7 @@
 
 lemma quotient_compose_list_gen:
   assumes a: "Quotient r2 abs2 rep2"
-  and     b: "equivp r2" (* reflp should be enough... *)
+  and     b: "equivp r2" (* reflp is not enough *)
   shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2))
                (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
   unfolding Quotient_def comp_def