eliminated extraneous wrapping of public records; tuned;

tuned signature; tuned;

renamed functor HeapFun to Heap;

misc tuning and clarification;

structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;

modernized structure names;

show direct GC time (which is included in CPU time);

eliminated obsolete C/flip combinator;

added List.nth

tuned make parameters for sunbroy2;

accomodate old version of "tail", e.g. on sunbroy2;

settings for parallel experimental Poly/ML 5.3;

sharpened name

more explicit notion of canonized code equations

more explicit notion of canonized code equations

tuned whitespace

tuned whitespace

dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology

merged

deactivated Datatype.distinct_simproc

dropped Datatype.distinct_simproc; tuned

order conjunctions to be printed without parentheses

approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability

merged

added add_tyconames; tuned

merged

more appropriate abstraction over distinctness rules

merged