src/HOL/Library/Quotient_Option.thy
changeset 53010 ec5e6f69bd65
parent 51994 82cc2aeb7d13
child 53012 cb82606b8215
--- a/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -50,12 +50,6 @@
   "option_rel (op =) = (op =)"
   by (simp add: option_rel_unfold fun_eq_iff split: option.split)
 
-lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
-  by (metis option.exhaust) (* TODO: move to Option.thy *)
-
-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_rel_mono[relator_mono]:
   assumes "A \<le> B"
   shows "(option_rel A) \<le> (option_rel B)"