# HG changeset patch
# User haftmann
# Date 1236416791 -3600
# Node ID 0d07f4823d3a3ce0c003fa98dcbfb0c1ad824df5
# Parent  32ccef17d4080f4b19be53b097955bc96025e269
drop poisonous code equations

diff -r 32ccef17d408 -r 0d07f4823d3a src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Sat Mar 07 10:06:12 2009 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Sat Mar 07 10:06:31 2009 +0100
@@ -24,7 +24,18 @@
   "~~/src/HOL/ex/Records"
 begin
 
-lemma [code, code del]: "(term_of \<Colon> 'a Predicate.pred \<Rightarrow> term) = term_of" ..
+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 *}