added ML_prf;

use_text/use_file now depend on explicit ML name space;

ML name space -- dummy version of Poly/ML 5.2 facility.

added ML-Systems/ml_name_space.ML;

use ML_prf within proofs;

local @{context};

moved global ML bindings to global place;

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

updated generated file;

wf_finite_psubset[simp], in_finite_psubset[simp]

Public interface to interpretation morphism.

moved term_of syntax to separate theory

removed obsolete theory

added quickcheck.ML

tuned comments;

multithreading for Poly/ML 5.1 is no longer supported;

tuned;

updated system manual;

Proof General / Emacs interface wrapper;

Proof General: option -I is obsolete;

added PROOFGENERAL_HOME;

separate emacs tool for Proof General / Emacs;

added quickcheck stub

removed babel again

celver code lemma avoid type ambiguity problem with Haskell

a sophisticated char/nibble conversion combinator

moved term_of syntax to separate theory

SimpleThread.fork;

Simplified thread fork interface.

added Concurrent/simple_thread.ML;

updated generated file;

misc tuning and modernization;

check setting and tool; added file;

Clearer separation of interpretation frontend and backend.

No interpretation of locale with dangling type frees.

Do not rely on locale assumption in interpretation.

The metis method now fails in the usual manner, rather than raising an exception, if it determines that it cannot prove the theorem.

Fixed typo in locale declaration.

added babel

explicit size of characters

dropped superfluous code lemmas

evaluation using code generator

generic value command

converted symbols.tex;

tuned;

converted misc.tex;

tuned;

generated files;