# HG changeset patch
# User haftmann
# Date 1236757546 -3600
# Node ID 14f469e70eab89e0143db1736a9f87f5b610ba02
# Parent  dfd31c1db060143b7b83982b6655289e1149b89b
explicitly delete some code equations

diff -r dfd31c1db060 -r 14f469e70eab src/HOL/FunDef.thy
--- 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"
diff -r dfd31c1db060 -r 14f469e70eab src/HOL/Library/Multiset.thy
--- 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
diff -r dfd31c1db060 -r 14f469e70eab src/HOL/ex/ExecutableContent.thy
--- 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