# HG changeset patch
# User kleing
# Date 1050404131 -7200
# Node ID 3c0a340be5143a8b8c8f3d71662da77cfdd1dcb8
# Parent  f5c3750292f5501832f90a91e4e8a67cd3e95308
fixed document

diff -r f5c3750292f5 -r 3c0a340be514 src/HOL/Map.thy
--- 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)"