renamed structure ValueParse to Parse_Value; eliminated old-style structure alias V;

refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;

renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;

renamed Outer_Parse to Parse (in Scala);

renamed Outer_Keyword to Keyword (in Scala);

avoid open Conv;

less pervasive names from structure Thm;

less pervasive names from structure Thm;

tuned;

merged

add real_le_linear to list of legacy theorem names

make SML/NJ happy

removed unused conversions;

tuned header; tuned white space;

moved normarith.ML where it is actually used; less inaccurate dependencies;

incorporated further conversions and conversionals, after some minor tuning;

eliminated redundant runtime checks;

normalize atyp names after unconstrainT, which may rename atyps arbitrarily;

more precise dependencies for HOL-Word-SMT_Examples;

merged

merge

added Sledgehammer documentation to TOC

added some Sledgehammer news

document Nitpick changes

merge

added Sledgehammer manual; some material was recovered from the Isar material, the rest is new

renamed Sledgehammer options

renamed options

remove support for crashing beta solver HaifaSat

renamed two Sledgehammer options

merged

added listsum lemmas

Revert mixin patch due to inacceptable performance drop.

add "no_atp"s to Nitpick lemmas

query _HOME environment variables at run-time, not at build-time

move Refute dependency from Plain to Main

move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong

recognize new Kodkod error message syntax

improve precision of set constructs in Nitpick

produce more potential counterexamples for subset operator (cf. quantifiers)

improved Sledgehammer proofs

pass "full_type" argument to proof reconstruction

made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code

delect installed ATPs dynamically, _not_ at image built time

Fix syntax; apparently constant apply was introduced in an earlier changeset.

Merged.

Add mixin to base morphism, required by class package; cf ab324ffd6f3d.

Remove improper use of mixin in class package.

Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1

use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document

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

include iszero_simps in semiring_norm just once (they are already included in rel_simps)

fix duplicate simp rule warning

no more RealPow.thy (remaining lemmas moved to RealDef.thy)

merged

simplify code for emptiness check

removed lemma real_sq_order; use power2_le_imp_le instead

merged

merged

represent de-Bruin indices simply by position in list

tuned reification functions