merged

slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;

use pointfree characterisation for fold_set locale

discontinued global config options within attribute name space;

more precise warnings: observe context visibility;

modernized structure Rule_Insts;

discontinued old / unused addss' (cf. 57f364d1d3b2);

eliminated global Unsynchronized.ref; eliminated Display.string_of_thm_without_context;

proper runtime context for auto_inv_tac;

simplified BLAST_DATA;

proper Proof.context -- eliminated global operations;

just one universal Proof.context -- discontinued claset/clasimpset;

modernized functor names; tuned;

method "deepen" with optional limit;

merged

removed redundant type annotations and duplicate examples

clarified map_simpset versus Simplifier.map_simpset_global;

make ZF_cs snapshot after final setup;

proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;

do not open ML structures;

eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);

misc tuning and simplification;

tuned proof;

tuned proof;

proper method_setup;

proper method_setup "split_idle";

proper method_setup "enabled";

simplified clasimpset declarations -- prefer attributes;

reduce the number of mono iterations to prevent the mono code from going berserk

tuned comment