--- 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