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";
use_thys [
"Integration",
"Isar",
"Local_Theory",
"Logic",
"ML",
"ML_old",
"Prelim",
"Proof",
"Syntax",
"Tactic"
];