schedule: more precise task model; removed obsolete structure Task;

fixed DESCRIPTION: single line; proper quoting of shell variables;

updated;

adapted ThyLoad.check_thy;

dropped

explizit checking for pattern discipline

proper handling of empty datatypes

improved class target: now considers class intro rules

new access interface in defs.ML

adaptions for code generation

proper implementation of rational numbers

localized of_nat

tuned

re-eliminated Option.thy

updated

PGIP change: thyname is optional in opentheory, markup even in case of header parse failure

Typo in comment

discontinued attached ML files; end_theory: fail on unresolved dependencies;

simplified ThyLoad.deps_thy etc.: discontinued attached ML files;

load_thy: try_ml_file unconditionally;

* Theory loader: old-style ML proof scripts are considered a legacy feature;

check_deps: really do reload the master text if required; load_thy: more robust check of corrupted deps; require_thy: outdate_thy if required; tuned;

Useful abbreviation of isatool commands used by Eclipse

thread-safeness: when creating certified items, perform Theory.check_thy *last*; tuned datatype proof;

Code to undo the function ascii_of

Fixing the code to undo the function ascii_of

metis

tuned ML setup;