--- a/src/HOL/Complex/ex/MIR.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Mon Aug 13 21:22:37 2007 +0200
@@ -5778,9 +5778,10 @@
"test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
- in SML to Mir
-
-code_gen mircfrqe mirlfrqe in SML to Mir file "raw_mir.ML"
+ in SML module_name Mir
+
+(*code_gen mircfrqe mirlfrqe
+ in SML module_name Mir file "raw_mir.ML"*)
ML "set Toplevel.timing"
ML "Mir.test1 ()"