dropped superfluous code theorems
authorhaftmann
Fri Jan 25 14:54:44 2008 +0100 (2008-01-25)
changeset 2596674f6817870f9
parent 25965 05df64f786a4
child 25967 dd602eb20f3f
dropped superfluous code theorems
src/HOL/HOL.thy
src/HOL/Library/AssocList.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/HOL.thy	Fri Jan 25 14:54:41 2008 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Jan 25 14:54:44 2008 +0100
     1.3 @@ -1210,7 +1210,7 @@
     1.4  
     1.5  constdefs
     1.6    simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
     1.7 -  "simp_implies \<equiv> op ==>"
     1.8 +  [code func del]: "simp_implies \<equiv> op ==>"
     1.9  
    1.10  lemma simp_impliesI:
    1.11    assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
     2.1 --- a/src/HOL/Library/AssocList.thy	Fri Jan 25 14:54:41 2008 +0100
     2.2 +++ b/src/HOL/Library/AssocList.thy	Fri Jan 25 14:54:44 2008 +0100
     2.3 @@ -97,14 +97,6 @@
     2.4  lemmas [simp del] = compose_hint
     2.5  
     2.6  
     2.7 -subsection {* Lookup *}
     2.8 -
     2.9 -lemma lookup_simps [code func]: 
    2.10 -  "map_of [] k = None"
    2.11 -  "map_of (p#ps) k = (if fst p = k then Some (snd p) else map_of ps k)"
    2.12 -  by simp_all
    2.13 -
    2.14 -
    2.15  subsection {* @{const delete} *}
    2.16  
    2.17  lemma delete_def:
     3.1 --- a/src/HOL/List.thy	Fri Jan 25 14:54:41 2008 +0100
     3.2 +++ b/src/HOL/List.thy	Fri Jan 25 14:54:44 2008 +0100
     3.3 @@ -199,7 +199,7 @@
     3.4  
     3.5  definition
     3.6    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
     3.7 -  "list_all2 P xs ys =
     3.8 +  [code func del]: "list_all2 P xs ys =
     3.9      (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
    3.10  
    3.11  definition