src/HOL/Map.thy
changeset 14376 9fe787a90a48
parent 14300 bf8b8c9425c3
child 14537 e95ba267e3d5
     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"