src/HOL/Map.thy
changeset 7958 f531589c9fc1
parent 5300 2b1ca524ace8
child 10137 d1c2bef01e2f
     1.1 --- a/src/HOL/Map.thy	Wed Oct 27 19:29:47 1999 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Oct 27 19:32:19 1999 +0200
     1.3 @@ -19,8 +19,6 @@
     1.4  map_of	:: "('a * 'b)list => 'a ~=> 'b"
     1.5  map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
     1.6  	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
     1.7 -
     1.8 -
     1.9  syntax
    1.10  map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.11  					         ("_/'(_/|->_')"   [900,0,0]900)