src/HOL/Map.thy
changeset 44921 58eef4843641
parent 44890 22f665a2e91c
child 46588 4895d7f1be42
     1.1 --- a/src/HOL/Map.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Map.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -265,7 +265,7 @@
     1.4  lemma map_comp_empty [simp]:
     1.5    "m \<circ>\<^sub>m empty = empty"
     1.6    "empty \<circ>\<^sub>m m = empty"
     1.7 -by (auto simp add: map_comp_def intro: ext split: option.splits)
     1.8 +by (auto simp add: map_comp_def split: option.splits)
     1.9  
    1.10  lemma map_comp_simps [simp]:
    1.11    "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
    1.12 @@ -354,7 +354,7 @@
    1.13  by (simp add: restrict_map_def)
    1.14  
    1.15  lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
    1.16 -by (auto simp add: restrict_map_def intro: ext)
    1.17 +by (auto simp add: restrict_map_def)
    1.18  
    1.19  lemma restrict_map_empty [simp]: "empty|`D = empty"
    1.20  by (simp add: restrict_map_def)
    1.21 @@ -485,7 +485,7 @@
    1.22  subsection {* @{term [source] dom} *}
    1.23  
    1.24  lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
    1.25 -by(auto intro!:ext simp: dom_def)
    1.26 +  by (auto simp: dom_def)
    1.27  
    1.28  lemma domI: "m a = Some b ==> a : dom m"
    1.29  by(simp add:dom_def)