more precise dependencies

updated SMT certificates

layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable

integrated SMT into the HOL image

replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite

use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)

split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)

added tracing of reconstruction data

added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms

deleted SMT translation files (to be replaced by a simplified version)

move the addition of extra facts into a separate module

normalize numerals: also rewrite Numeral0 into 0

added missing rewrite rules for natural min and max

rewrite bool case expressions as if expression

simplified normalize_rule and moved it further down in the code

merged addition of rules into one function

added simplification for distinctness of small lists

moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)

added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;

conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;

the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;

avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;

raise Fail uniformly for proofterm errors, which appear to be rather low-level;

unconstrainT operations on proofs, according to krauss/schropp;

added Proofterm.get_name variants according to krauss/schropp; tuned signature;

conditional structure SingleAssignment;

merged

merged

tuned proofs and fact and class names

tuned fact collection names and some proofs

grouped local statements

tuned test problems

merged

merged

simplified proof

modernized specifications;

updated/unified some legacy warnings;

tuned;

do not emit legacy_feature warnings here -- users have no chance to disable them;

removed obsolete CVS Ids;

removed some obsolete admin stuff;

check NEWS;

removed obsolete CVS Ids;

updated some version numbers;

minor tuning;

reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only; (Spelling note: "supersede" is indeed more common in Isabelle sources, although "supercede" is also correct according to major dictionaries.)

merged

merged

modernized specifications; tuned reification

merged

added lemmas concerning last, butlast, insort

Remove RANGE_WARN

clarified NEWS entry

merged

added NEWS entry

Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'

Add rules directly to the corresponding class locales instead.

Removed usage of normalizating locales.

speed up some proofs, fixing linarith_split_limit warnings

fix some linarith_split_limit warnings