made more of the transition from "CookBook" to "ProgTutorial"
theory Baseimports Mainuses "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