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 925 8d51795ef54d
parent 920 dae99175f584
child 930 68c1f378a70a 
--- a/Quot/QuotMain.thy	Mon Jan 25 20:35:42 2010 +0100
+++ b/Quot/QuotMain.thy	Mon Jan 25 20:47:20 2010 +0100
@@ -111,7 +111,7 @@
 
 text {* Lemmas about simplifying id's. *}
 lemmas [id_simps] =
-  id_def[symmetric, THEN eq_reflection]
+  id_def[symmetric]
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_o[THEN eq_reflection]
nominal2