keep normal size for %mlref tag;

basic setup for ML antiquotations -- with rail diagrams; tuned;

eliminated "Toplevel control", which belongs to TTY/ProofGeneral model;

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

misc tuning;

more on Isabelle/ML;