# 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 \ 'a Predicate.pred \ 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 \ 'a::{type, term_of} Predicate.pred \ Code_Eval.term) = Code_Eval.term_of" .. +lemma [code, code del]: + "(Code_Eval.term_of \ 'a::{type, term_of} Predicate.seq \ Code_Eval.term) = Code_Eval.term_of" .. text {* However, some aren't executable *}