--- a/src/HOL/Map.thy Tue Apr 01 16:08:34 2003 +0200
+++ b/src/HOL/Map.thy Tue Apr 01 17:43:10 2003 +0200
@@ -11,7 +11,6 @@
types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
consts
-empty :: "'a ~=> 'b"
chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
dom :: "('a ~=> 'b) => 'a set"
@@ -20,6 +19,7 @@
map_upds:: "('a ~=> 'b) => 'a list => 'b list =>
('a ~=> 'b)" ("_/'(_[|->]_/')" [900,0,0]900)
syntax
+empty :: "'a ~=> 'b"
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
("_/'(_/|->_')" [900,0,0]900)
@@ -31,13 +31,13 @@
("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
translations
+ "empty" => "_K None"
+ "empty" <= "%x. None"
"m(a|->b)" == "m(a:=Some b)"
defs
-empty_def "empty == %x. None"
-
chg_map_def "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"