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