merged

prefer p2e before e2p; use measure_unique_Int_stable_vimage;

add auto support for AE_mp

add borel_fubini_integrable; remove unused bijectivity rules for measureable functions

parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;

Task_Queue.update_timing: more precise treatment of interruptibility; Task_Queue.waiting: potentially expensive wait dependencies are subject to trace flag;

Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;

thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;

tuned comments;

clarified Proofterm.proofs_enabled;

explicit is better than implicit;

tuned odd conditional expression;

eliminated slightly odd abstract type Task_Queue.deps; tuned signature; tuned;

merged

Introduction of metis calls and other cosmetic modifications.

merged

avoid ML structure aliases (especially single-letter abbreviations)

making the bash script swipl_version closer to Isabelle's conventional bash scripts

the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv. introduced binder variants for simple_integral, positive_integral and integral.

merged

scala serializer adds parentheses around function literals

made SML/NJ happy

term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)

refined Task_Queue.dequeue_deps (more incremental);

maintain Task_Queue.group within Task_Queue.task; Task_Queue.dummy_task: id = 0 in accordance to Document.no_id etc.; tuned signature;

tuned comment;

Future.join_results: discontinued post-hoc recording of dynamic dependencies; abstract Task_Queue.deps; tuned signature; tuned;

more informative task timing: some dependency tracking;

refined task timing: joining vs. waiting; tuned;

simplified trace;

more specific Goal.fork_name;

name "passive" tasks (practically lazy values);

tuned trivial cases;

tuned signature; tuned vacous forks;

support named tasks, for improved tracing;

more direct Future.bulk, which potentially reduces overhead for Par_List; tuned signature;

tuned isatest settings;

added basic task timing;

some notes on Cygwin;

more platform hints;

merged

tuned;

back to post-release mode;

removed obsolete test tags;

removed Florian's email from isatest (bounces)

merged

use pre-image measure, instead of image

use AE_mp in AE_conjI proof

tuned proof

merged

moved theorem

restructured theory; tuned proofs

merged

Gauge measure removed

merged

report mutabelle log in mira configuration

back to post-release mode;

delete .elc files unconditionally -- they cause too many incompatibilities;

Added tag Isabelle2011 for changeset 6d736d983d5c

clarified example settings for Proof General;

adhoc patches relative to ProofGeneral-4.1pre101216, which has setprefs working;

more precise stats;

some adhoc patches for ProofGeneral-4.1pre110112;

enforce STIXGeneral, which is preferred by PG 4.1;

default UTF-8 locale, to work with funny base directory (e.g. Chinese);

enforce fonts;

added option -f FONT;

Proof General 4.x interface wrapper;

old Proof General patches;

Added tag isa2011-test3 for changeset 55a45051b220

Tuned definition of sdiv.

CRITICAL markup for critical poking with unsynchronized references;

Replaced smod by standard mod operator to reflect actual behaviour of the SPARK tools.

cancel document execution before editing, to improve reactivity on systems with few cores;

tuned isatest settings (for Poly/ML SVN 1278);

merged

do not restore old files on startup, which is potentially slow due to automatic rechecking; attempt to enable thick caret for improved visibility;

singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);

workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;

improved README -- Isabelle symbols and fonts;

delete compiled .elc files to improve portability on Linux, notably for GNU Emacs 23.1.x instead of 23.2.x;

do not overwrite proof-shell-quit-timeout by default (final PG 4.1 supposedly gets it right);

Added tag isa2011-test2 for changeset 237328506a42

Documented unused_thms

JVM/Windows: more robust treatment of unicode in file names;

java/scala: default to UTF-8;

updated Named_Target.init;

made SML/NJ happy;

Word: direct conversion wrt. LargeInt to bypass exception Overflow;

fixing list_to_set_comprehension simproc

more release checks;

potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);

clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;

added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;

merged

tuned;

Cygwin: back to ProofGeneral-3.7.1.1 with XEmacs, since PG 4.x with GNU Emacs 23 is painfully slow;

isabelle jedit as alternative;

Apple's way of locating java;

more notes on final release stage;

makedist: refer to isabelle-release;

Added tag isa2011-test1 for changeset 7d035da21e9c

tuned;

some announcement;

tuned;

merged

made Z3 the default SMT solver again

some notes on final release stage;

isatest: run at-poly on macbroy28 for slightly more robust isatest-doc;

keep Proof General 4.0 and 3.7.1.1 for now;

tuned;

misc updates for release;