eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
eliminated Isar toplevel invocation functions, which belong to TTY/ProofGeneral model;
moved remaining "ML toplevel" material to "Compile-time context";
theory Baseimports Pureuses "../../antiquote_setup.ML"beginend