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;

fixed imports from ../../Auth;

turned Unify flags into configuration options (global only);

usedir: added options -M -T for multithreading;

removed 'declare' from tactic emulations;

theory loader: removed obsolete update_thy (coincides with use_thy); tuned; tuned comments;

theory loader: removed obsolete update_thy (coincides with use_thy);

theory loader: added use_thys, removed obsolete update_thy;

theory loader: added use_thys, removed obsolete update_thy; various global ML references of Pure and HOL have been turned into configuration options;

Issue a warning, when "function" encounters variables occuring in function position, as in "f (g x) = ..." where g is a variable.

more error handling

added more instances;

simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"

split off Option theory

new nbe implementation

more robust simproces

tuned