src/HOL/Map.thy
changeset 53015 a1119cf551e8
parent 46588 4895d7f1be42
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/Map.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  definition
     1.6    map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
     1.7 -  "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"
     1.8 +  "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) = (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"
     1.9  
    1.10  nonterminal maplets and maplet
    1.11