more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;

some support for thy_load_commands; clarified signatures;

tuned signature;

clarified initialization of Thy_Load, Thy_Info, Session;

tuned;

more robust cleaning of "% tag" and "-- cmt";

some support for inlining file content into outer syntax token language;

tuned comment;

tuned;

added keyword kind "thy_load" (with optional list of file extensions);

updated generated files;

more strict syntax, according to manual;

abstracted lemma

retain unknown options within preferences; tuned print;

more comprehensible platform family name;

tuned message;

fewer components, more roots;

actually remove makeall (cf. 292b97e17fb7);

tuned;

Backed out changeset ec82c33c75f8;

Typo fixed.

merged

merged

fixed lemmas

abstracted lemmas

updated to new init_components, hoping that mira can digest that;

some explanations on component categories;

specific cygwin components;

obsolete;

some explanations on isabelle components;

some grouping of components;

renamed components to components_old, to make room for some directory of the same name;

minor robustification;

added "isabelle components" tool;

tuned;

direct support for component forests via init_components; explicit ISABELLE_COMPONENTS_MISSING;

allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira; clarified spaces in file names -- ISABELLE_HOME is non-critical after abolishment of "make";

tuned;

tuned;

updated component repository;

updates on 32 bit vs. 64 bit platforms; added Mountain Lion; dropped Leopard; tuned;

updated to jedit_build-20120813, pointing to another contrib directory as a change;

merged

tuned proofs;

look in current directory first before looking up includes in the TPTP directory, as required by Geoff

prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala

more robust multi-platform support;

updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;

support for jdk-7u6 component;

Clarification: free variables allowed in interpreted locale instances.

merged

fixed proof

abstracted lemmas

Backed out changeset 6cf7a9d8bbaf

abstracted lemmas

merged

Turned into Admin tool download_components.

tuned;

tuned;

some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");

tuned;

fixed handling of "int" in the wake of its port to the quotient package

removed dead code

merged

Added various options, notably -c to download components listed in Admin/components. Also, curl instead of wget.

ignore some administrative files on newer Mercurial versions as well;

some support for persistent user preferences;

merged

explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;

more direct interpretation of document_variants for build (unchanged for usedir);

tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0

fixed then-else confusion

tweak Vampire setup in the light of new evaluation

improved set of reconstructor methods

warn users about unused "using" facts

be less aggressive at kicking out chained facts

recognize bus errors as crash

consider removing chained facts last, so that they're more likely to be kept

clarified format of etc/options: only declarations, not re-definitions;

check_errors for cumulative session content;

even more defensive path expansion (see also 8d381fdef898);

support for 'typ' with explicit sort constraint;

added jedit option -d;

always retain doc-src (as regular component);

merged

Calling isabelle with proper (relative) path, no longer relying on $PATH.

fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;

updated to jedit-4.5.2 (still unchanged);

restored ISABELLE_OUTPUT etc -- still relevant at least for mira.py itself

tuned;

fixed mira.py (cf. fd50596bf78b)

more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;

more static antiquotations;

always show some timing information, to reduce the need for explicit -v;

some information for central Isabelle repository configuration;

reduced settings patching