# HG changeset patch
# User nipkow
# Date 1529299632 -7200
# Node ID 8dea233d4baedb84124a3cdeb9ab4a9bc7f897b7
# Parent  0eb751466b792142ad25cc99238b54af557a71c4# Parent  b047339bd11cc85e2bfa9ada31064934a6d9028b
merged

diff -r 0eb751466b79 -r 8dea233d4bae src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Jun 17 22:01:16 2018 +0100
+++ b/src/HOL/Map.thy	Mon Jun 18 07:27:12 2018 +0200
@@ -133,6 +133,10 @@
     by (induction xys) simp_all
 qed simp
 
+lemma empty_eq_map_of_iff [simp]:
+  "empty = map_of xys \<longleftrightarrow> xys = []"
+by(subst eq_commute) simp
+
 lemma map_of_eq_None_iff:
   "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
 by (induct xys) simp_all
diff -r 0eb751466b79 -r 8dea233d4bae src/HOL/Option.thy
--- a/src/HOL/Option.thy	Sun Jun 17 22:01:16 2018 +0100
+++ b/src/HOL/Option.thy	Mon Jun 18 07:27:12 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>