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;