src/HOL/Map.thy
changeset 28562 4e74209f113e
parent 26443 cae9fa186541
child 28790 2efba7b18c5b
     1.1 --- a/src/HOL/Map.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4    by simp_all
     1.5  
     1.6  defs
     1.7 -  map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
     1.8 +  map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
     1.9  
    1.10  
    1.11  subsection {* @{term [source] empty} *}