# HG changeset patch
# User haftmann
# Date 1221549686 -7200
# Node ID 4f06fae6a55e59f41fd48548cbc911f05c29d25b
# Parent  7ebe8dc06cbb297c142de663df3ae671128189a5
dropped superfluous code lemmas

diff -r 7ebe8dc06cbb -r 4f06fae6a55e src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Tue Sep 16 09:21:24 2008 +0200
+++ b/src/HOL/Equiv_Relations.thy	Tue Sep 16 09:21:26 2008 +0200
@@ -93,9 +93,8 @@
 
 subsection {* Quotients *}
 
-constdefs
-  quotient :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/'/" 90)
-  "A//r == \<Union>x \<in> A. {r``{x}}"  -- {* set of equiv classes *}
+definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"  (infixl "'/'/" 90) where
+  [code func del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
 
 lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
   by (unfold quotient_def) blast
diff -r 7ebe8dc06cbb -r 4f06fae6a55e src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Tue Sep 16 09:21:24 2008 +0200
+++ b/src/HOL/Library/Word.thy	Tue Sep 16 09:21:26 2008 +0200
@@ -2267,6 +2267,8 @@
   fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
     fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
 
+declare fast_bv_to_nat_helper.simps [code func del]
+
 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
     fast_bv_to_nat_helper bs (Int.Bit0 bin)"
   by simp
diff -r 7ebe8dc06cbb -r 4f06fae6a55e src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Tue Sep 16 09:21:24 2008 +0200
+++ b/src/HOL/NatBin.thy	Tue Sep 16 09:21:26 2008 +0200
@@ -18,7 +18,7 @@
 begin
 
 definition
-  nat_number_of_def [code inline]: "number_of v = nat (number_of v)"
+  nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)"
 
 instance ..
 
diff -r 7ebe8dc06cbb -r 4f06fae6a55e src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Tue Sep 16 09:21:24 2008 +0200
+++ b/src/HOL/ex/ExecutableContent.thy	Tue Sep 16 09:21:26 2008 +0200
@@ -11,7 +11,6 @@
   Binomial
   Commutative_Ring
   Enum
-  Eval
   List_Prefix
   Nat_Infinity
   Nested_Environment
@@ -20,19 +19,10 @@
   Primes
   Product_ord
   SetsAndFunctions
-  State_Monad
   While_Combinator
   Word
   "~~/src/HOL/ex/Commutative_Ring_Complete"
   "~~/src/HOL/ex/Records"
 begin
 
-lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
-declare fast_bv_to_nat_helper.simps [code func del]
-
-setup {*
-  Code.del_funcs
-    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))
-*}
-
 end