src/HOL/Map.thy
changeset 25965 05df64f786a4
parent 25670 497474b69c86
child 26443 cae9fa186541
     1.1 --- a/src/HOL/Map.thy	Fri Jan 25 14:53:58 2008 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Jan 25 14:54:41 2008 +0100
     1.3 @@ -83,6 +83,13 @@
     1.4    "map_of [] = empty"
     1.5    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
     1.6  
     1.7 +declare map_of.simps [code del]
     1.8 +
     1.9 +lemma map_of_Cons_code [code]: 
    1.10 +  "map_of [] k = None"
    1.11 +  "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
    1.12 +  by simp_all
    1.13 +
    1.14  defs
    1.15    map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    1.16