--- 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)"
--- 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:
--- 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