src/HOL/Map.thy
changeset 5195 277831ae7eac
parent 5183 89f162de39cf
child 5300 2b1ca524ace8
     1.1 --- a/src/HOL/Map.thy	Fri Jul 24 14:53:23 1998 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Jul 24 17:18:15 1998 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  consts
     1.6  empty   :: "'a ~=> 'b"
     1.7 -update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
     1.8 +map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
     1.9             ("_/[_/|->/_]" [900,0,0] 900)
    1.10  override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.11  dom     :: "('a ~=> 'b) => 'a set"
    1.12 @@ -22,7 +22,7 @@
    1.13  syntax (symbols)
    1.14    "~=>"     :: [type, type] => type
    1.15                 (infixr "\\<leadsto>" 0)
    1.16 -  update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.17 +  map_upd    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.18                 ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
    1.19    override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    1.20                 (infixl "\\<oplus>" 100)
    1.21 @@ -30,7 +30,7 @@
    1.22  defs
    1.23  empty_def "empty == %x. None"
    1.24  
    1.25 -update_def "m[a|->b] == %x. if x=a then Some b else m x"
    1.26 +map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
    1.27  
    1.28  override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.29