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%);

Isabelle font, based on TeX glyhps;

enable future_scheduler by default;

ISABELLE_USEDIR_OPTIONS: -M max is default;

unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;

removed spurious exception_trace;

print_theorems: more robust difference, even after finished proof;

export context_node;

merged

more antiquotations;

pcpodef package: state two goals, instead of encoded conjunction;

recovered goal_pat;

inhabitance goal is now stated in original form and result contracted -- the previous attempt with contracted goal and initial unfolding did not work, because it disrupted the Isar proof structure (e.g. ?thesis);

tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.; more antiquotations; explicit Theory.requires; adapted to recent changes in ~~/src/HOL/Tools/typedef_package.ML; misc tuning and simplification;

add_typedef: unfold set_def in tactical proof as well;

merged

Theory.checkpoint before commencing proof;

misc tuning and modernisation;

merged

logically separate typedef axiomatization from constant definition

add def before setting up goal

killed dead code

constrain type inference to sort "type"

merged.

cleaned up some proofs in Cfun.thy

implement cont_proc theorem cache using theory data

use ML antiquotations

clean up diff_bin_simps

move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs

fixed import: requires ContNotDenum;

fixed import: requires ContNotDenum;

requires RComplete;

merged.

move all neg-related lemmas to NatBin; make type of neg specific to int

separate neg_simps from rel_simps

use {less,le}_number_of in integer simprocs

use lemma lists defined in Int.thy

Merged.

Satisfy a_axioms.

Merged.