Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/QuotMain.thy
changeset 911 95ee248b3832
parent 909 3e7a6ec549d1
child 919 c46b6abad24b 
--- a/Quot/QuotMain.thy	Thu Jan 21 11:11:22 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 21 12:03:47 2010 +0100
@@ -101,7 +101,7 @@
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp bexeq_rsp
+lemmas [quot_respect] = quot_rel_rsp
 lemmas [quot_equiv] = identity_equivp
 
 (* Lemmas about simplifying id's. *)
nominal2