tuned import

dropped dead code

terminate after first exception -- avoid syslog flooding;

avoid buffer loading overrun; tuned;

merged

collecting all axioms in a locale context in quickcheck; adding some verbose output;

choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing

removing finiteness goals

adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets

Symbol.encode header edits;

merged

tuned whitespace

more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)

Removal of obsolete ML bindings

more robust locking;

proper update_header;

refined node_header -- more direct buffer access (again);

merged

improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case

fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction

more robust set element extractor

fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates

tuned proofs;

more tolerant cygpath invocation, allow empty CLASSPATH;

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);