src/HOL/Map.thy
changeset 22744 5cbe966d67a2
parent 22230 bdec4a82f385
child 24331 76f7a8c6e842
     1.1 --- a/src/HOL/Map.thy	Fri Apr 20 11:21:41 2007 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Apr 20 11:21:42 2007 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
     1.5  
     1.6  defs
     1.7 -  map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
     1.8 +  map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
     1.9  
    1.10  
    1.11  subsection {* @{term [source] empty} *}