dropped superfluous code theorems
authorhaftmann
Fri, 25 Jan 2008 14:54:44 +0100 (2008-01-25)
changeset 25966 74f6817870f9
parent 25965 05df64f786a4
child 25967 dd602eb20f3f
dropped superfluous code theorems
src/HOL/HOL.thy
src/HOL/Library/AssocList.thy
src/HOL/List.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)"
--- 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