src/HOL/Library/AssocList.thy
changeset 25966 74f6817870f9
parent 23373 ead82c82da9e
child 26152 cf2cccf17d6d
     1.1 --- a/src/HOL/Library/AssocList.thy	Fri Jan 25 14:54:41 2008 +0100
     1.2 +++ b/src/HOL/Library/AssocList.thy	Fri Jan 25 14:54:44 2008 +0100
     1.3 @@ -97,14 +97,6 @@
     1.4  lemmas [simp del] = compose_hint
     1.5  
     1.6  
     1.7 -subsection {* Lookup *}
     1.8 -
     1.9 -lemma lookup_simps [code func]: 
    1.10 -  "map_of [] k = None"
    1.11 -  "map_of (p#ps) k = (if fst p = k then Some (snd p) else map_of ps k)"
    1.12 -  by simp_all
    1.13 -
    1.14 -
    1.15  subsection {* @{const delete} *}
    1.16  
    1.17  lemma delete_def: