more robust: no failure on bad rule;

tuned;

more accurate delete operation via authentic index --- minor performance tuning;

minor performance tuning;

clarified signature: do not expose internal data structures;

clarified signature;

clarified signature: prefer canonical order (latest declarations first);

clarified print order: follow original classical.ML, before 8aa1c98b948b;

maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;

tuned: order does not matter here;

clarified modules;

clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);

more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation; avoid costly Item_Net.length, which is linear in size;

tuned proof;

clarified modules;

redundant: Net.DELETE already handled;

tuned;

clarified signature: more explicit types, notably (thm option) instead of (thm list);

more robust: unique result expected, otherwise index calculations will go wrong;

tuned;

tuned;

clarified signature: anticipate use in src/Provers/classical.ML;

clarified signature;

tuned source structure;

efficient rule declarations in canonical order, for update of netpairs and print operation;

added option `-S` to Mirabelle to specify the subgoal classes to consider

moved to more appropriate theory

more correct lemma name

merged

added basic support for persistent prover data to Sledgehammer