# HG changeset patch
# User nipkow
# Date 1075951838 -3600
# Node ID 9fe787a90a48bd88b58c3dae19b9c415294cc529
# Parent  a545da363b23a8f53648817544caa16be7cad80b
Changed variable names.

diff -r a545da363b23 -r 9fe787a90a48 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Feb 04 03:44:05 2004 +0100
+++ b/src/HOL/Map.thy	Thu Feb 05 04:30:38 2004 +0100
@@ -81,7 +81,7 @@
 dom_def: "dom(m) == {a. m a ~= None}"
 ran_def: "ran(m) == {b. EX a. m a = Some b}"
 
-map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
+map_le_def: "m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2  ==  ALL a : dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a"
 
 primrec
   "map_of [] = empty"