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;

misc tuning;

CONTRIBUTORS

fact consolidation

more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;

merged

command 'print_term_bindings' supersedes 'print_binds';

Proof General legacy;

removed obsolete "isabelle unsymbolize";

minor renovation of slightly odd and old README;

sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;

tweaking

correctly take weights into consideration

tuned whitespace and parentheses

use right theory name for theorems in evaluation driver

killed dead code

reintroduced 'extra features' + only print message in verbose mode

got rid of hard-coded weights, now that we have TFIDF

tuning

tuning

reintroduced 'extra features' but with lower weight than before (to account for tfidf)

resolution modulo double negation

compile

merged two small theory files

tuned variable names

whitespace tuning

repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side

tiny refinements

suppress documentation "how_to_prove_it" for now, notably for release;

updated to jdk-7u60 -- back to stable Java 7 for Isabelle2014 release;

updated generated file;

merged

updated cygwin on server; include unzip, which is required for src/Doc/JEdit;

tuning

reintroduced MaSh hints, this time as persistent creatures