append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)

avoid loop in 'all_class_pairs' (caused by e.g. loading the 'Ceta' theory and calling Sledgehammer with the two facts 'fun_of_map.cases' and 'Lattices.bounded_lattice_top_class.sup_top_left' with a polymorphic type encoding)

merged

added lemmas

improved docs

made SML/NJ happier

got rid of a pointer equality

get rid of some pointer equalities

tuned terminology

improvements to the machine learning algos (due to Cezary K.)

added lemma

refactor some tactics

refactor some tactics

add helper function map_prod

document property 'rel_cases'

generate 'rel_cases' theorem for (co)datatypes

update for release;

Added tag Isabelle2014-RC0 for changeset 251ef0202e71

merged

modernized definitions;

proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);

CONTRIBUTORS

refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply; uniform appearance of xsymbol and HTML output for sums

misc tuning for release;

tuned;

NEWS

prefer ac_simps collections over separate name bindings for add and mult

added Tom's hyp_subst update

reduced name variants for assoc and commute on plus and mult

tuned;

insist in explicit overloading;

more uniform names;

misc tuning for release;

revived unchecked theory (see cebaf814ca6e);

suppress completion of obscure keyword;

tuned;

misc tuning for release;

NEWS;

Tail recursion no longer supported by "function".

merged

weaker assumption for "list_emb_trans"; added lemma

added monotonicity lemma for list embedding

no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)

renamed "list_hembeq" into slightly shorter "list_emb"

misc tuning;

merge

document property 'rel_intros'

generate 'rel_intros' theorem for (co)datatypes

Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.

tuned grammar and spelling (cf. 0cf15843b82f);

document property 'corec_code'

generate 'corec_code' theorem for codatatypes

modernized definitions;

misc tuning and clarification;

check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;

optional exit hook for theory-like targets

restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game

centralized (ad-hoc) switching of targets in named_target.ML

add lemmas: polynomial div/mod distribute over addition

reverted 9512b867259c -- appears to break 'metis'

clarified "axiomatization" -- minor rewording of this delicate concept;

tuned;

more on ML options; suppress somewhat old Pretty.margin_default;

redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;

overdue NEWS concerning c4daa97ac57a

Merge

for new release

merge

document property 'rel_induct'

generate 'rel_induct' theorem for datatypes

fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too

added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'

whitespace tuning

robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)

use context instead of theory

fine-tuned methods

tuned message

updated docs

changed default MaSh engine

removed needless code

speed up MaSh a bit

mix NB and kNN

tuned (reordered) code

clean up MaSh export a bit

clean up MaSh evaluation driver

merged

tuned;

clarified quasi-generic PIDE;

misc updates for release;

more release notes;

Library/Tree: bst is preferred to be a function

Library/Tree: use datatype_new, bst is an inductive predicate

more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

some lemmas about the indicator function; removed lemma sums_def2

generate type correct terms in uncheck phase

updated to sumatra_pdf-2.5.2;

ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);

removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;

tuned comments;

updated README;

"isabelle tty" is superseded by "isabelle console";

tuned description: fit into 80 chars terminal;

qualified String.explode and String.implode

removed non-existing MaSh component from list

modernized diagnostic options

use SMT2

compile

tuning

killed Python version of MaSh, now that the SML version works adequately

tracing facilities for the code generator preprocessor

tuned interface

corrected handled exception

proper trading of variables; more appropriate ML variable names

modernized

jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;

removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);

updated NEWS -- removed material that is already in the manual;

merged

misc tuning;