Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 07 Jan 2010 16:51:38 +0100
changeset 823 ae3ed7a68e80
parent 822 5527430f9b6f
child 824 cedfe2a71298
Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
Quot/Examples/AbsRepTest.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2