tuned text

corrected nonsensical associativity of `` and dvd

add exponential and uniform distributions

fundamental theorem of calculus for the Lebesgue integral

add Int_atMost

more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;

fork slow part of Thy_Load.body_files only;

explore theory_body_files via future, for improved performance; further internalization of header errors;

merged

use proper entry point for MaSh in test driver

export ATP and Isar commands separately

proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);

discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;

discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;

updated README;

documentation for isabelle build_dialog and its implicit use in isabelle jedit;

clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL); added jedit option -n to bypass build_dialog;

avoid startup within GUI thread -- it is only required later for dialog; tuned signature;

more uniform default logic, using settings, options, args etc.; clarified build_dialog -C: imitate jEdit logic selection more precisely;

use right names in MePo exporter

parse more liberal MaSh suggestion syntax (for the eval driver)

merged

made Python code compile again (by Daniel K.)

tweaked MaSh proximity

reduce max number of dependencies for MaSh to get rid of junk

more feature tweaks

prioritize chained facts

more MaSh feature tweaking

record free variables as a MaSh feature

expand type classes into their ancestors for MaSh

tweaked MaSh features, based on comments by Josef Urban

increase weight of local facts again (MaSh)

simplify code now that "mash.py" supports weights

added weights to MaSh (by Daniel Kuehlwein)

Move the measurability prover to its own file

Show search depth in the debug output of the measurability prover

Remove looping rule from measurability prover

rules for improper Lebesgue integrals (using tendsto at_top)

take proximity into account for MaSh + fix a debilitating bug in feature generation

tuning

clarified default button (cf. org/gjt/sp/jedit/gui/OptionsDialog.java);

select logic session names, not paths;

added keyboard shortcut for button (canonical way to do that?);

evade ugly default font, notably on Windows laf;

center main window;

more direct dialog via existing GUI components;

clarified logic argument: session name, not path name; tuned;

tuned message;

implicit build_dialog for Isabelle/jEdit; clarified option -l: refer to session name, not image path;

tuned message;

tuned OK feedback;

check for existing image (even if outdated); removed conflicting "clean" option;

more elementary dialog, with less interaction;

basic interaction with build process;

allow to terminate jobs via Progress; tuned;

more formal progress context;