explicitly revoke delay, to avoid spurious timer events after deactivation of related components;

clarified document nodes (full import graph) vs. node_status (non-preloaded theories); tuned;

more defensive node_header;

clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;

SMT fails if the chosen SMT solver is not installed

merged

speed up Sledgehammer's clasimpset lookup a bit

use SPASS instead of E for Metis examples -- it's seems faster for these small problems

spelling

avoid undeclared variables in let bindings; tuned proofs;

tuned proofs;

more release tests;

display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);

Finish localizing the quotient package.

merged

Added infrastructure for mapping SPARK field / constructor names to Isabelle types

Use long prefix rather than short package name to disambiguate constant names introduced by verification environment

more explicit development graph;

removed dead code (cf. a34d89ce6097);

tuned proofs;

tuned proofs;

removed introiff (cf. b09afce1e54f);

tuned;

removed broken/unused introiff (cf. d452117ba564);

discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);

tuned;

tuned proofs;

prefer uniform Timing.message -- avoid assumption about sequential execution;

prefer final ADTs -- prevent ooddities;

more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);