Changed variable names.
authornipkow
Thu Feb 05 04:30:38 2004 +0100 (2004-02-05)
changeset 143769fe787a90a48
parent 14375 a545da363b23
child 14377 f454b3004f8f
Changed variable names.
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Wed Feb 04 03:44:05 2004 +0100
     1.2 +++ b/src/HOL/Map.thy	Thu Feb 05 04:30:38 2004 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  dom_def: "dom(m) == {a. m a ~= None}"
     1.5  ran_def: "ran(m) == {b. EX a. m a = Some b}"
     1.6  
     1.7 -map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
     1.8 +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"
     1.9  
    1.10  primrec
    1.11    "map_of [] = empty"