CookBook/Base.thy
changeset 160 cc9359bfacf4
parent 106 bdd82350cf22
child 161 83f36a1c62f2
--- a/CookBook/Base.thy	Wed Mar 04 14:26:21 2009 +0000
+++ b/CookBook/Base.thy	Thu Mar 05 16:46:43 2009 +0000
@@ -15,5 +15,9 @@
       Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
 *}
 
+ML {*
+  fun warning str = str
+  fun tracing str = str
+*}
 
 end