src/HOL/Map.thy
changeset 13890 90611b4e0054
parent 12919 d6a0d168291e
child 13908 4bdfa9f77254
     1.1 --- a/src/HOL/Map.thy	Tue Apr 01 16:08:34 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Apr 01 17:43:10 2003 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4  types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
     1.5  
     1.6  consts
     1.7 -empty	::  "'a ~=> 'b"
     1.8  chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     1.9  override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.10  dom	:: "('a ~=> 'b) => 'a set"
    1.11 @@ -20,6 +19,7 @@
    1.12  map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    1.13  	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
    1.14  syntax
    1.15 +empty	::  "'a ~=> 'b"
    1.16  map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.17  					         ("_/'(_/|->_')"   [900,0,0]900)
    1.18  
    1.19 @@ -31,13 +31,13 @@
    1.20  				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
    1.21  
    1.22  translations
    1.23 +  "empty"    => "_K None"
    1.24 +  "empty"    <= "%x. None"
    1.25  
    1.26    "m(a|->b)" == "m(a:=Some b)"
    1.27  
    1.28  defs
    1.29  
    1.30 -empty_def    "empty == %x. None"
    1.31 -
    1.32  chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.33  
    1.34  override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"