diff -r 455a9f89c47d -r 7aa35601ff65 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Thu May 24 14:20:23 2012 +0200
@@ -46,10 +46,16 @@
 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
   by (metis option.exhaust) (* TODO: move to Option.thy *)
 
-lemma option_reflp[reflp_preserve]:
+lemma option_reflp[reflexivity_rule]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp
 
+lemma option_left_total[reflexivity_rule]:
+  "left_total R \<Longrightarrow> left_total (option_rel R)"
+  apply (intro left_totalI)
+  unfolding split_option_ex
+  by (case_tac x) (auto elim: left_totalE)
+
 lemma option_symp:
   "symp R \<Longrightarrow> symp (option_rel R)"
   unfolding symp_def split_option_all option_rel.simps by fast