--- a/src/HOL/Map.thy Wed Jan 04 17:04:11 2006 +0100
+++ b/src/HOL/Map.thy Wed Jan 04 19:22:53 2006 +0100
@@ -530,7 +530,7 @@
lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
apply(rule ext)
-apply(force simp: map_add_def dom_def not_None_eq split:option.split)
+apply(force simp: map_add_def dom_def split:option.split)
done
subsection {* @{term [source] ran} *}
@@ -587,13 +587,13 @@
done
lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
- by (fastsimp simp add: map_le_def not_None_eq)
+ by (fastsimp simp add: map_le_def)
lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
-by (fastsimp simp add: map_le_def map_add_def dom_def not_None_eq)
+by (fastsimp simp add: map_le_def map_add_def dom_def)
lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)