--- a/NEWS Tue Aug 04 15:00:58 2015 +0200
+++ b/NEWS Tue Aug 04 23:11:16 2015 +0200
@@ -172,6 +172,9 @@
*** HOL ***
+* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
+been removed. INCOMPATIBILITY.
+
* Quickcheck setup for finite sets.
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
--- a/src/HOL/Map.thy Tue Aug 04 15:00:58 2015 +0200
+++ b/src/HOL/Map.thy Tue Aug 04 23:11:16 2015 +0200
@@ -137,12 +137,6 @@
"(map_of xys x = None) = (x \<notin> fst ` (set xys))"
by (induct xys) simp_all
-lemma map_of_is_SomeD: "map_of xys x = Some y \<Longrightarrow> (x,y) \<in> set xys"
-apply (induct xys)
- apply simp
-apply (clarsimp split: if_splits)
-done
-
lemma map_of_eq_Some_iff [simp]:
"distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
apply (induct xys)
@@ -229,7 +223,7 @@
done
lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
-by (induct xs) (simp, atomize (full), auto)
+ by (induct xs) (auto split: if_splits)
lemma map_of_mapk_SomeI:
"inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>