--- a/Quot/QuotMain.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -166,6 +166,9 @@
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection, symmetric]
+  id_o[THEN eq_reflection]
+  o_id[THEN eq_reflection] 
+
 
 section {* Methods / Interface *}