Eta-expanded some declarations that are illegal under value polymorphism

Replaced obsolete "use" command

Uses Basis Library equivalent of cd

Makefile improvements by Thomas Santen and Stephan Herrmann Should be more portable across different versions of make

if_cancel added to HOL_ss

Removed or eta-expanded some declarations that are illegal under value polymorphism

Checks for empty files. Replaces auto() calls

Eta-expansion of a function definition, for value polymorphism

Structure Bool and value Int.toString needed to replace makestring calls

Eta-expansion of a function definition, for value polymorphism

Eta-expansion of a function definition, for value polymorphism

Removal of needless function definition

Eta-expansion of a function definition, for value polymorphism

Added instructions on starting up

New material from Norbert Voelker for efficient binary comparisons

A bit of commutative ing theory, with a simplification tacxtic and an example.

Added Lagrang. Modified comment.

Replaced LK&Modal by Sequents

Updating of a reference (Ch. Paulin)

Minor textual improvements; updating of a reference

Have been obsolete for months; contents are now in Shared and NS_Shared

Basis library emulation for old ML compilers

Added warning message

Tidied up some proofs, ...

Minor reformatting

Further comments on versions of SML/NJ

plus -> Plus to avoid hiding class plus

restored changed prettyprinting of ==>;