dropped old Library/Word.thy and toy example ex/Adder.thy

dropped old Library/Word.thy and toy example ex/Adder.thy

do not open Legacy by default;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;

renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;

tuned;

tuned signature;

renamed class Outer_Lex to Token and Token_Kind to Token.Kind;

centralized legacy aliases;

prefer structure Parse_Spec;

renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;

renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;

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