src/HOL/Map.thy
changeset 17782 b3846df9d643
parent 17724 e969fc0a4925
child 18447 da548623916a
     1.1 --- a/src/HOL/Map.thy	Fri Oct 07 22:59:18 2005 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Oct 07 22:59:19 2005 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4    --"requires amssymb!"
     1.5  
     1.6  translations
     1.7 -  "empty"    => "_K None"
     1.8 +  "empty"    => "%_. None"
     1.9    "empty"    <= "%x. None"
    1.10  
    1.11    "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"