--- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 29 15:00:40 2010 +0200
@@ -3209,13 +3209,12 @@
interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
interpret_floatarith_sin
-code_reflect
+code_reflect Float_Arith
datatypes float = Float
and floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
| Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num
and form = Bound | Assign | Less | LessEqual | AtLeastAtMost
functions approx_form approx_tse_form approx' approx_form_eval
- module_name Float_Arith
ML {*
fun reorder_bounds_tac prems i =
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Apr 29 15:00:40 2010 +0200
@@ -1909,9 +1909,8 @@
ML {* @{code cooper_test} () *}
-code_reflect
+code_reflect Generated_Cooper
functions pa
- module_name Generated_Cooper
file "~~/src/HOL/Tools/Qelim/generated_cooper.ML"
oracle linzqe_oracle = {*
--- a/src/HOL/Decision_Procs/MIR.thy Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Apr 29 15:00:40 2010 +0200
@@ -5791,9 +5791,8 @@
ML {* @{code test4} () *}
ML {* @{code test5} () *}
-(*code_reflect
+(*code_reflect Mir
functions mircfrqe mirlfrqe
- module_name Mir
file "mir.ML"*)
oracle mirfr_oracle = {* fn (proofs, ct) =>
--- a/src/HOL/Predicate.thy Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Predicate.thy Thu Apr 29 15:00:40 2010 +0200
@@ -880,10 +880,9 @@
code_abort not_unique
-code_reflect
+code_reflect Predicate
datatypes pred = Seq and seq = Empty | Insert | Join
functions map
- module_name Predicate
ML {*
signature PREDICATE =