prefer tactics with explicit context;

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

removed old CVS Ids;
tuned headers;

parameterize assoc_fold with is_numeral predicate

joined theories IntDef, Numeral, IntArith to theory Int

canonical prefixing of class constants

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

Goal.prove;

Simplifier.inherit_context instead of Simplifier.inherit_bounds;

simprocs: Simplifier.inherit_bounds;

renamed sg_ref to thy_ref;

Deleted Library.option type.

Polymorphic treatment of binary arithmetic using axclasses

use Tactic.prove instead of prove_goalw_cterm in internal proofs!

sane interface for simprocs;

use tracing function for trace output;

do not pass theory values, but sg_ref;

global timing flag;

improved name of simproc;

new simprocs assoc_fold and combine_coeff