fixed document
authorkleing
Tue Apr 15 12:55:31 2003 +0200 (2003-04-15)
changeset 139123c0a340be514
parent 13911 f5c3750292f5
child 13913 b3ed67af04b8
fixed document
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Mon Apr 14 18:52:45 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Apr 15 12:55:31 2003 +0200
     1.3 @@ -325,9 +325,9 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 -section{* @{text"\<subseteq>\<^sub>m"} *}
     1.8 +section {* map\_le *}
     1.9  
    1.10 -lemma [simp]: "empty \<subseteq>\<^sub>m g"
    1.11 +lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
    1.12  by(simp add:map_le_def)
    1.13  
    1.14  lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"