use parallel map

tweak MaSh fudge factors

more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"

basic monitor panel, using the powerful jfreechart library; sorted Isabelle menu entries -- this is mainly a catalog;

added jfreechart library, including the old version of iText from its distribution (required for the demo application and examples);

check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);

make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);

final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;

adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;

obsolete;

eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005); \usepackage{proof} only where required;

merged

deactivate actual fork -- unstable in scala-2.9.2 on multicore hardware;

some support to recover from spurious crash -- this is Physics, not Mathematics;

avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;

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;

basic wrapper for session build dialog;

tuned;

tuned signature in accordance to document operations;

tuned;

merged

\<noteq> now has the same associativity as ~= and =

tweaked order of theorems to avoid forward dependencies (MaSh)

rationalized MaSh evaluation harness

more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions

added feature weights in MaSh

promote local facts using a hack (for MaSh)

proper action labels, to make this appear in the "Shortcuts" panel, for example;

turned off noisy MaSh features

added MaSh learning to Mirabelle

fixed bug in initialization of naive Bayes (MaSh)

tuned MaSh exporter -- and don't make temp directories unless explicitly told so

generalized MaSh exporter to sets of theories

remove SMT proofs in Multivariate_Analysis

prove tendsto_power_div_exp_0 * * * missing rename

add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2

merged

emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);

go back to Z3 3.2

tuned defs of sec_xyz

provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;

simplify MaSh term patterns + add missing global facts if there aren't too many

MaSh improvements: deeper patterns + more respect for chained facts

tuned names

tweaked MaSh exporter

renamed "Type.thy" to something that's less likely to cause conflicts

proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)

added "fact_filter" option to Mirabelle

tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)

some notes on the Isabelle component repository at TUM;

use filterlim in Lim and SEQ; tuned proofs

conversion rules for at, at_left and at_right; applied to l'Hopital's rules.

weakened assumptions for lhopital_right_0

tuned proof

add L'Hôpital's rule

add filterlim rules for exp and ln to infinity

add filterlim rules for inverse and at_infinity

add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image

add filterlim rules for unary minus and inverse

rename filter_lim to filterlim to be consistent with filtermap

add check to Cooper's algorithm that left-hand of dvd is a numeral

merged

robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer

avoid odd warnings due to failure of systray icon;

synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic); clarified signature -- cache init is unsynchronized and hopefully used at most once per file;