CONTRIBUTORS

added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)

added Isabelle system option 'mash'

updated cygwin;

afford strict check (see also AFP/a8e08d947f0a);

add various lemmas

merged

merged

adhoc move to lxbroy10, which has 120 GB more memory than lxbroy2;

explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;

news

updated docs

more flexible environment variable

tuning

added unit :: linorder

added lemma

implemented MaSh/SML hints

better way to take invisible facts into account than 'island' business

cleaner handling of learned proofs

implemented learning of single proofs in SML MaSh

take weights into consideration in knn

added SML implementation of MaSh

use E 1.8's auto scheduler option

started work on MaSh/SML

tune

store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution

trace windows uses search feature of Pretty_Text_Area; recursive invocations and intermediate steps are now shown in order; refinements to the exclusion of uninteresting subtraces in the output

obsolete -- always pdf;

prefer T1 with searchable underscore (requires proper cm-super fonts);

merged

some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus;

re-focus target explicity, e.g. relevant for Sledgehammer panel;

clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;

more explicit identification for more robust adhoc change of environment /home/isatest/.isabelle/etc/settings -- notably for $ISABELLE_PLATFORM64;

renamed positive_integral to nn_integral

hide more consts to beautify documentation

fixed document generation for HOL-Probability

introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces

document property 'disc_map_iff'

generate 'disc_map_iff[simp]' theorem for (co)datatypes

fix 'set_empty' theorem when the discriminator is 'op ='

typos

tuned comments;

clarified dependencies -- Mavericks presently does not work;

clarified docking layout, amending 9c2ca698690e;

correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs

removed needless transfer

use 'simp add:' syntax in Sledgehammer rather than 'using'

silence methods even better

honor original format of conjecture or hypotheses in Z3-to-Isar proofs

proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;

added lemmas for -1

proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')

new syntax for card, normalized spacing for #

clarified stylized status of sandwich algebra

dropped dead code

accurate separation of static and dynamic context

syntactic means to prevent accidental mixup of static and dynamic context

proper separation of static and dynamic context

optimization for trivial cases

modernized setup

dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor

unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches

normalize type variables of evaluation term by conversion

more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)

new approach to silence proof methods, to avoid weird theory/context mismatches

type

merged

restrict default docking layout to bare minimum -- NB: Simplifier Trace still needs fine-tuning to show up on demand;

updated isatest;

updated to polyml-5.5.2;

practically obsolete: plain "poly" should work, except for Linux without libgmp installed;

updated to polyml-5.5.2;

document 'set_empty'

generate 'set_empty' theorem for BNFs

document 'map_id0'

note map_id0 more often

added lemma

added lemmas

transfer theorems since 'silence_methods' may change the theory

add mono rules for diff

clean up Lebesgue integration

more bnf_decl -> bnf_axiomatization

tuned docs

hide more internal names

tuning

no reset for 'end' -- e.g. relevant for 'notepad';

updated keywords

bnf_decl -> bnf_axiomatization

tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";

Replaced refute with nitpick.

NEWS;

tuned message;

smarter recovery from toplevel type error;

more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion; prefer JDialog for FloatingWindowContainer, to keep it in front of the main window; updated to Navigator.jar 2.5, SideKick.jar 1.6;

updated keywords;

merged

more markup;

more position markup to help locating the query context, e.g. from "Info" dockable;

always bounce focus back to main text area, unless explicit focus component is given here (see also 7b65f4da136d);

tuned signature;

delete attribute for code abbrev

dropped term_of obfuscation -- not really required; tuned theory structure

hardcoded nbe and sml into value command

modernized setups

degeneralized value command into HOL

dimiss simplified as evaluator due to little practical relevance

prefer separate command for approximation

removed junk from library theory

note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs

normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;

tuned GUI;

clarified detach_operation: ignore empty output;

bounce focus back to main text area -- Output is for output, not query input;

update for release;

merged

tuned message;

no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;

some position markup to help locating the query context, e.g. from "Info" dockable;

tuned GUI;