reverted unsound optimization

got rid of one of two Metis variants

tuning

unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer

killed needless pass

dependency reporting for code generation errors

more abstract dictionary construction

reduced prominence of "permissive code generation"

split rules for of_bool, similar to if

don't forget the last inference(s) after conjecture skolemization

centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)

keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized

renamed Sledgehammer options for symmetry between positive and negative versions

more robust w.r.t. exceptions raised by proof methods

tuning

compile

tuning

added 'algebra' and 'meson' to 'try0'

made 'try0' (more) silent

'using' already uses the new Skolemizer, enabling a subtly shorter syntax

merged

extended cardinals library

define ofilter outside of wo_rel

more direct simplification rules for 1 div/mod numeral; added simplification rules for (- 1) div/mod numeral

systematically suppress tracing if asked for (affects 'meson' proof method)

silenced reconstructors in Sledgehammer

proper 'show' detection

correctly handle exceptions arising from (experimental) Isar proof code

made smlnj happy

Merge

Removed a dependence upon Old_Number_Theory. Simplified a few proofs.

merged

made tactic more robust

Merge

minor adjustments

added Dmitriy, since he did the case syntax

Replacing the theory Library/Binomial by Number_Theory/Binomial

Merge

converting to new Number_Theory

tuned;

tuned signature;

obsolete

more suitable names, without any notion of "activating"

discontinued obsolete attribute "standard";

tuned signature;

less clumsy namespace

immediate "activation" of const syntax at declaration time

avoid (now superfluous) indirect passing of constant names

prefer explicit code symbol type over ad-hoc name mangling

more abstract syntax passing

more abstract declaration of unqualified constant names in code printing context

merged

explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;

prefer explicit 'for' context;

prefer self-contained user-space tool;

define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;

NEWS for 31afce809794;

reverted cb17feba74e0, avoid sweeping garbage under the carped (MaSh should not create .pyc files anymore, see also 778b2b8f4a35, 347f743e8336);

semicolon is minor keyword (see also 29f1e53f9937);

tuned proof;

more user aliases;

propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;

simplified inner syntax;

added lemma

Merge

Restored Suc rather than +1, and using Library/Binimial

killed 'More_BNFs' by moving its various bits where they (now) belong

hide 'csum' etc.

installed by Johannes in Extended now

merged

hide Fin in output of value via postprocessor; no hinding needed elsewhere

hide extended.Fin in code generator output

no document for Cartouche_Examples: avoid problems typesetting "\001";

NEWS;

merged

tuned;

observe local syntax mode (according to e3a39dae2004, which was lost in 0f3ad56548bc), e.g. relevant for "abbreviation (output)" with non-terminating syntax;

clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;

Locales paper has appeared in print.

tuned spelling;

removed junk;

merged

tuned;

prefer rail cartouche -- avoid back-slashed quotes; proper documentation of \<newline> syntax;

tuned signature;

avoid breakdown of document preparation, which does not understand cartouche tokens yet;

more cartouche examples, including uniform nesting of sub-languages;

inner syntax token language allows regular quoted strings; tuned signature;

tuned signature;

tuned error messages, more accurate position;

tuned -- more direct err_prefix;

clarified scan_cartouche_depth, according to Scala version; more accurate error position;

tuned errors;

whitespace tuning

whitespace tuning

made SML/NJ happier