clarified bootstrapping of Pure;

tuned errors;

prefer File.full_path in accordance to check_file;

more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;

updated Thy_Load.check_thy;

refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;

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;