tuned;

tuned;

proper context;

simplified simproc programming interfaces;

prefer tactics with explicit context;

proper context;
tuned whitespace;

simplifier uses proper Proof.context instead of historic type simpset;

dropped unused argument – avoids problem with SML/NJ

tuned signature;

removed old CVS Ids;
tuned headers;

simplified type int (eliminated IntInf.int, integer);

tuned integers

prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
tuned;

simprocs: no theory argument -- use simpset context instead;

simprocs: Simplifier.inherit_bounds;

Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ

Move towards standard functions.

Deleted Library.option type.

adapted type of simprocs;

adhoc_freeze_vars;

tries harder to remove negative literals, e.g.
-2*x = 0 goes to x=0 rather than -x=0.

simproc for cancelling common factors around = < <= div /