removed obsolete Class.class_of_locale/locale_of_class;

tuned;

added add_def;

added is_class; tuned signature of add_const/abbrev_in_class; removed obsolete class_of_locale/locale_of_class; tuned name prefixing: Sign.full_name does the job;

PolyML.Compiler.maxInlineSize := 80;

abbrev: return hypothetical def; replaced obsolete Theory.add_finals_i by Theory.add_deps; misc cleanup;

renamed def to define; abbrev: return hypothetical def;

(un)overload: full rewrite; use Attrib.attribute_i for internal args; misc tuning;

add_abbrevs: unvarify result;

replaced obsolete Theory.add_finals_i by Theory.add_deps;

Theory.specify_const: added deps argument;

renamed LocalTheory.def to LocalTheory.define;

typo in comment fixed

significant code overhaul, bugfix for inductive data types

added generic provide_file; tuned;

pass explicit target record -- more informative peek operation; removed obsolete hide_abbrev; misc tuning;

more informative TheoryTarget.peek operation;

fork_mixfix: explicit bool argument;

eval_term: moved actual evaluation out of CRITICAL section;

preventing eta-redexes in theorems from causing failure

trying to make it run faster

calling the correct interface

replaced syntax/translations by abbreviation;

updated

dropped local_syntax

tuned

(intermediate quickfix)

removed