tuned comments; back to fast String.compare (almost no difference in performance);

tuned comments;

tuned names of start_timing,/end_timing/check_timer; removed obsolete ML compatibility fragments;

removed obsolete ML compatibility fragments;

avoid strange typing problem in MosML;

tuned names of start_timing,/end_timing/check_timer;

simplified local theory wrappers;

removed mapping; added reinit;

simplified exit; added reinit;

simplified LocalTheory.exit;

Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented

deleted all uses of sign_of as it's now the identity function

tuned;

tuned Variable.trade;

introduces canonical AList functions for loop_tacs

minor refinements

redundancy checkes includes eta-expansion

improved syntax

added bounded_linear and bounded_bilinear locales

no special treatment for cygwin (this is supposed to be actual cygwin, not win32 polyml within cygwin);

tuned comments;

added x86-cygwin;

oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.

LocalTheory.restore;

init: '-' refers to global context; provide reinit operation;

abbrevs: return result; LocalTheory.restore;

Stack.map_top;

abbrevs: return result; separate reinit/restore;

separate map_top/all;

abbrevs: return result (use LocalTheory.abbrevs directly);