--- a/Quot/QuotOption.thy	Fri Jan 08 14:43:30 2010 +0100
+++ b/Quot/QuotOption.thy	Fri Jan 08 15:02:12 2010 +0100
@@ -80,4 +80,22 @@
   apply(simp only: option_rel_some[OF a])
   done
 
-end
\ No newline at end of file
+lemma option_map_id[id_simps]: "option_map id \<equiv> id"
+  apply (rule eq_reflection)
+  apply (rule ext)
+  apply (case_tac x)
+  apply (auto)
+  done
+
+lemma option_rel_eq[id_simps]: "option_rel op = \<equiv> op ="
+  apply (rule eq_reflection)
+  apply (rule ext)+
+  apply (case_tac x)
+  apply auto
+  apply (case_tac xa)
+  apply auto
+  apply (case_tac xa)
+  apply auto
+  done
+
+end