src/HOL/Option.thy

--- a/src/HOL/Option.thy	Sun Jun 17 13:10:14 2018 +0200
+++ b/src/HOL/Option.thy	Sun Jun 17 20:31:51 2018 +0200
@@ -36,6 +36,9 @@
 lemma not_Some_eq [iff]: "(\<forall>y. x \<noteq> Some y) \<longleftrightarrow> x = None"
   by (induct x) auto
 
+lemma comp_the_Some[simp]: "the o Some = id"
+by auto
+
 text \<open>Although it may appear that both of these equalities are helpful
 only when applied to assumptions, in practice it seems better to give
 them the uniform iff attribute.\<close>