--- a/src/HOL/FunDef.thy Wed Mar 11 08:45:46 2009 +0100
+++ b/src/HOL/FunDef.thy Wed Mar 11 08:45:46 2009 +0100
@@ -225,10 +225,10 @@
subsection {* Concrete orders for SCNP termination proofs *}
definition "pair_less = less_than <*lex*> less_than"
-definition "pair_leq = pair_less^="
+definition [code del]: "pair_leq = pair_less^="
definition "max_strict = max_ext pair_less"
-definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
-definition "min_strict = min_ext pair_less"
+definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition [code del]: "min_strict = min_ext pair_less"
definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
lemma wf_pair_less[simp]: "wf pair_less"
--- a/src/HOL/Library/Multiset.thy Wed Mar 11 08:45:46 2009 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Mar 11 08:45:46 2009 +0100
@@ -1487,7 +1487,7 @@
by auto
definition "ms_strict = mult pair_less"
-definition "ms_weak = ms_strict \<union> Id"
+definition [code del]: "ms_weak = ms_strict \<union> Id"
lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
--- a/src/HOL/ex/ExecutableContent.thy Wed Mar 11 08:45:46 2009 +0100
+++ b/src/HOL/ex/ExecutableContent.thy Wed Mar 11 08:45:46 2009 +0100
@@ -24,24 +24,6 @@
"~~/src/HOL/ex/Records"
begin
-lemma [code, code del]:
- "(size :: 'a::size Predicate.pred => nat) = size" ..
-lemma [code, code del]:
- "pred_size = pred_size" ..
-lemma [code, code del]:
- "pred_case = pred_case" ..
-lemma [code, code del]:
- "pred_rec = pred_rec" ..
-lemma [code, code del]:
- "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
-lemma [code, code del]:
- "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
-
-text {* However, some aren't executable *}
-
-declare pair_leq_def[code del]
-declare max_weak_def[code del]
-declare min_weak_def[code del]
-declare ms_weak_def[code del]
+declare min_weak_def [code del]
end