CookBook/Base.thy
changeset 189 069d525f8f1d
parent 188 8939b8fd8603
child 190 ca0ac2e75f6d
--- a/CookBook/Base.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-theory Base
-imports Main
-uses
-  "chunks.ML"
-  "antiquote_setup.ML"
-begin
-
-(* to have a special tag for text enclosed in ML *)
-ML {*
-
-val _ =
-  OuterSyntax.command "ML" "eval ML text within theory"
-    (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
-    (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