more symbols;

proper context for "net" tactics;
avoid implicit Tactic.build_net -- make its operational behavior explicit in application;

proper context for assume_tac (atac remains as fall-back without context);

proper context for match_tac etc.;

more explicit Method.modifier with reported position;

tuned whitespace;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

standardized aliases;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

modernized structure Object_Logic;

eliminated some unused/obsolete Args.bang_facts;

modernized structure Context_Rules;

dropped redundant gen_ prefix

eliminated dead code;

modernized method setup;

unified type Proof.method and pervasive METHOD combinators;

moved generic intuitionistic prover to src/Tools/intuitionistic.ML;