explicit EventBus for results; removed low-level get_result/try_result;

added methods "+" and "-"; event: non-synchronized execution of handlers, based on synchronized snapshot;

Generic event bus.

eliminated fun/val confusion

merged

clean up proofs of lemma Maclaurin

disabled old jedit plugin;

more markup elements;

more markup elements;

removed duplicate sum_case used only by function package; moved projections; hide (open)

tuned NEWS; CONTRIBUTORS

renamed LexOrds.thy to Termination.thy; examples for sizechange method

tuned;

merged

refined execute, which replaces exec/exec2;

maintain initial process environment; refined execute, which replaces exec/exec2; tuned;

merged

tackling simultaneous val/fun bindings

proper class IsabelleSystem -- no longer static; tuned;

PATH: /opt/local/bin is back again (required for latex etc.);

merged.

clean up lemmas about ln

clean up lemmas about exp

more proofs about differentiable

use less_iff_Suc_add instead of less_add_one

rearranged subsections; cleaned up some proofs

move theorems about limits from Transcendental.thy to Deriv.thy

cleaned up some proofs; removed redundant simp rules

move sin and cos to their own subsection

clean up some proofs; remove unused lemmas

tuned;

* Proofs of are run in parallel on multi-core systems; * High-level support for concurrent ML programming;

updated generated file;

updated thread-safe programming;

updated generated file;

added float_token, and num_const, float_const; tuned;

renamed terminal category "float" to "float_token", to avoid name space conflicts with actual "float" types in user theories (only "float_const" is encountered in practice anyway); tuned;

manual file type setup using AppHack 1.1;

target PWD;

updated scala path;

added platform_file; added find_logics;

proper -X option; relative result, do not insist in "$THIS/Isabelle.app";

unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result; tuned;

more sophisticated MacOS interface script (mostly for Carbon Emacs); no longer include MacPorts path; simplified default PROOFGENERAL_OPTIONS, removed PROOFGENERAL_EMACS;

updated web style for Mercurial 1.1.1;

misc webstyle adaptions;

updated web style for Mercurial 1.1;

removed Ids;

merged

removed Ids;

merged.

constdefs -> definition

removed Ids;

merged.

remove cvs Id tags

merged

basic setup for MacOS application bundle;

GHC ext pragma in generated Haskell modules

dropped Ids

temporary adaption to new locale code

restructured; circumvent sort problem

merged.

new theory Dsum: cpo of disjoint sum

scale dependency graph in document

changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions

proper document antiquotations;

merged

method "sizechange" proves termination of functions; added more infrastructure for termination proofs

future proofs: Future.fork_pri 1 minimizes queue length and pending promises -- slight improvement of throughput, at the cost of a bit of parallelism;

renamed structure TaskQueue to Task_Queue;

Future.fork_pri;

renamed structure TaskQueue to Task_Queue; tasks are ordered according to priority, which has been generalized from bool to int; removed unused focus; tuned dequeue: single pass due to proper priority order; tuned dequeue_towards;

renamed structure TaskQueue to Task_Queue;

renamed structure TaskQueue to Task_Queue; generalized fork_background to fork_pri; reduced tracing; map: inherit task priority; removed unused focus;

removed old scheduler;

tuned enqueue: plain add_edge, acyclic not required here;

tuned messages;

updated generated file;

repaired railroad accident;

updated generated files;

added 'atp_messages' command, which displays recent messages synchronously;

merged

flipped fold implementation

merged

codegen

code for {x:A. P(x)} and for fold

Testfile for Stefan's code generator

moved value.ML to src/Tools

\underscoreoff is now default

tuned some proofs

removed Ids;

merged

merged

merged

Unified syntax of nominal_primrec with the one used by fun(ction) and new version of primrec command.

Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.

merged

tuned comments; tuned;

tuned ML_OPTIONS for improved multicore performance;

refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;

requires: check ancestors directly;

Context.display_names;

global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;

usage: echo ML settings as well;

future proofs: more robust check via Future.enabled;

removed former Isabelle font (cf. IsabelleItalic);

incorporated isabelle-fonts side-branch (forced merge);

replaced single quote by mathematical prime;

generated file;

bold version: math glyphs from plain IsabelleMono;

fixed rangle;

use dash from text font, not math;

added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak); replaced old-style digits by bold ones (bf);

generated ttf;

renamed to IsabelleMono;

added README with original licenses;

renamed Isabelle to IsabelleItalic;

fixed rangle glyph;

the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;

Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);