more contributors;

separate section "Inspecting the syntax" for print_syntax;

misc tuning of inner syntax;

added inner lexical syntax, reusing outer one;

misc tuning;

tuned outer lexical syntax; fixed var/tvar: really need question marks here;

more tuning of Pure grammer;

updated and elaborated Pure grammer;

added Pure grammer (from old ref manual);

mixfix annotations: verbatim for special symbols;

added section "The Pure grammar" (incomplete version, based on old ref manual);

added section "Priority grammars" (variant from old ref manual);

added section "Co-regularity of type classes and arities" (variant from old ref manual); tuned arity spacing;

minor tuning (according to old ref manual);

misc tuning and rearrangement of section "Printing logical entities";

misc tuning and rearrangement of section "Printing logical entities";

fixed/tuned syntax for attribute "tagged";

added pretty printing options (from old ref manual);

separate chapter "Inner syntax --- the term language";

updated/refined types of Isar language elements, removed special LaTeX macros;

unified use of declaration environment with IsarImplementation; tuned ML decls;

ignore ThyOutput.source flag;

added bind_thm, bind_thms;

tuned section "Incorporating ML code"; moved method_setup to separate section "Defining proof methods";