# HG changeset patch
# User haftmann
# Date 1215076569 -7200
# Node ID 58b695d10cdf68e06ce49339487dfe117ef91e7f
# Parent  fb6a272fe5d0dfbf387ce0a45338f2d41446aaad
tuned

diff -r fb6a272fe5d0 -r 58b695d10cdf src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Thu Jul 03 11:16:08 2008 +0200
+++ b/src/HOL/ex/ExecutableContent.thy	Thu Jul 03 11:16:09 2008 +0200
@@ -31,28 +31,6 @@
 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]
 
-(*FIXME distribute to theories*)
-declare divides_def [code func del] -- "Univ_Poly"
-declare star_minus_def [code func del] -- "StarDef"
-declare Zseq_def [code func del]
-declare Bseq_def [code func del]
-declare monoseq_def [code func del]
-declare Cauchy_def [code func del]
-declare subseq_def [code func del]
-declare powhr_def [code func del]
-declare hlog_def [code func del]
-declare scaleHR_def [code func del]
-declare stc_def [code func del]
-declare increment_def [code func del]
-declare of_hypreal_def [code func del]
-declare HInfinite_def [code func del]
-declare is_starext_def [code func del]
-declare isNSUCont_def [code func del]
-declare isNSCont_def [code func del]
-declare isUCont_def [code func del]
-declare NSCauchy_def [code func del]
-declare NSBseq_def [code func del]
-
 setup {*
   Code.del_funcs
     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))