author | kleing |
Tue, 15 Apr 2003 12:55:31 +0200 | |
changeset 13912 | 3c0a340be514 |
parent 13911 | f5c3750292f5 |
child 13913 | b3ed67af04b8 |
src/HOL/Map.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Map.thy Mon Apr 14 18:52:45 2003 +0200 +++ b/src/HOL/Map.thy Tue Apr 15 12:55:31 2003 +0200 @@ -325,9 +325,9 @@ apply auto done -section{* @{text"\<subseteq>\<^sub>m"} *} +section {* map\_le *} -lemma [simp]: "empty \<subseteq>\<^sub>m g" +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)"