src/HOL/Map.thy
changeset 41229 d797baa3d57c
parent 39992 f225a499a8e5
child 41550 efa734d9b221
     1.1 --- a/src/HOL/Map.thy	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -50,8 +50,7 @@
     1.4    map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
     1.5    "(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.6  
     1.7 -nonterminals
     1.8 -  maplets maplet
     1.9 +nonterminal maplets and maplet
    1.10  
    1.11  syntax
    1.12    "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")