--- 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
--- 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
--- 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 ..
--- 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