changeset 161 | 83f36a1c62f2 |
parent 160 | cc9359bfacf4 |
--- a/CookBook/Base.thy Thu Mar 05 16:46:43 2009 +0000 +++ b/CookBook/Base.thy Fri Mar 06 16:12:16 2009 +0000 @@ -14,10 +14,10 @@ (OuterParse.ML_source >> (fn (txt, pos) => Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); *} - +(* ML {* fun warning str = str fun tracing str = str *} - +*) end