src/HOL/Map.thy

 apply auto
 apply (subgoal_tac "~ (aa = a) ")
 apply auto
 done
 
-section{* @{text"\<subseteq>\<^sub>m"} *}
-
-lemma [simp]: "empty \<subseteq>\<^sub>m g"
+section {* map\_le *}
+
+lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
 by(simp add:map_le_def)
 
 lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
 by(fastsimp simp add:map_le_def)