# HG changeset patch
# User haftmann
# Date 1201269284 -3600
# Node ID 74f6817870f9ae2cb3520350874f3612a315020c
# Parent  05df64f786a4834641d0b3da250fbac793461980
dropped superfluous code theorems

diff -r 05df64f786a4 -r 74f6817870f9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jan 25 14:54:41 2008 +0100
+++ b/src/HOL/HOL.thy	Fri Jan 25 14:54:44 2008 +0100
@@ -1210,7 +1210,7 @@
 
 constdefs
   simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
-  "simp_implies \<equiv> op ==>"
+  [code func del]: "simp_implies \<equiv> op ==>"
 
 lemma simp_impliesI:
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
diff -r 05df64f786a4 -r 74f6817870f9 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Fri Jan 25 14:54:41 2008 +0100
+++ b/src/HOL/Library/AssocList.thy	Fri Jan 25 14:54:44 2008 +0100
@@ -97,14 +97,6 @@
 lemmas [simp del] = compose_hint
 
 
-subsection {* Lookup *}
-
-lemma lookup_simps [code func]: 
-  "map_of [] k = None"
-  "map_of (p#ps) k = (if fst p = k then Some (snd p) else map_of ps k)"
-  by simp_all
-
-
 subsection {* @{const delete} *}
 
 lemma delete_def:
diff -r 05df64f786a4 -r 74f6817870f9 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 25 14:54:41 2008 +0100
+++ b/src/HOL/List.thy	Fri Jan 25 14:54:44 2008 +0100
@@ -199,7 +199,7 @@
 
 definition
   list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
-  "list_all2 P xs ys =
+  [code func del]: "list_all2 P xs ys =
     (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
 
 definition