eliminated clone;
authorwenzelm
Tue Aug 04 23:11:16 2015 +0200 (2015-08-04)
changeset 60841144523e0678e
parent 60840 9043fd2c8cb6
child 60842 5510c8444bc4
eliminated clone;
NEWS
src/HOL/Map.thy
     1.1 --- a/NEWS	Tue Aug 04 15:00:58 2015 +0200
     1.2 +++ b/NEWS	Tue Aug 04 23:11:16 2015 +0200
     1.3 @@ -172,6 +172,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
     1.8 +been removed. INCOMPATIBILITY.
     1.9 +
    1.10  * Quickcheck setup for finite sets.
    1.11  
    1.12  * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
     2.1 --- a/src/HOL/Map.thy	Tue Aug 04 15:00:58 2015 +0200
     2.2 +++ b/src/HOL/Map.thy	Tue Aug 04 23:11:16 2015 +0200
     2.3 @@ -137,12 +137,6 @@
     2.4    "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
     2.5  by (induct xys) simp_all
     2.6  
     2.7 -lemma map_of_is_SomeD: "map_of xys x = Some y \<Longrightarrow> (x,y) \<in> set xys"
     2.8 -apply (induct xys)
     2.9 - apply simp
    2.10 -apply (clarsimp split: if_splits)
    2.11 -done
    2.12 -
    2.13  lemma map_of_eq_Some_iff [simp]:
    2.14    "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
    2.15  apply (induct xys)
    2.16 @@ -229,7 +223,7 @@
    2.17  done
    2.18  
    2.19  lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
    2.20 -by (induct xs) (simp, atomize (full), auto)
    2.21 +  by (induct xs) (auto split: if_splits)
    2.22  
    2.23  lemma map_of_mapk_SomeI:
    2.24    "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>