| changeset 27103 | d8549f4d900b |
| parent 26515 | 4a2063a8c2d2 |
| child 27421 | 7e458bd56860 |
--- a/src/HOL/ex/ExecutableContent.thy Tue Jun 10 15:30:01 2008 +0200 +++ b/src/HOL/ex/ExecutableContent.thy Tue Jun 10 15:30:06 2008 +0200 @@ -34,4 +34,9 @@ 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