Added Extraction/Pigeonhole.

added Brian Hufmann's finite instances

Fixed bug in code generator for let and split leading to ill-formed code.

Adapted to new argument format of MinProof constructor.

Adapted to new interface og thms_of_proof / axms_of_proof.

Adapted to new interface of thms_of_proof.

- Tuned handling of oracles - Put arguments of axms_of_proof and thms_of_proof into "canonical order"

mentioned change to exp_ge_add_one_self, new transitivity rules

changes from renaming of exp_ge_add_one_self

renamed exp_ge_add_one_self to exp_ge_add_one_self_aux

renamed exp_ge_add_one_self2 to exp_ge_add_one_self

added extra transitivity rules

added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint

changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp

import FixedPoint instead of Gfp

removed Gfp

removed Lfp

combined Lfp and Gfp to FixedPoint

tuned ML_OPTIONS;

export clear_ss;

added unfold_tac (Simplifier.inherit_bounds);

simprocs: Simplifier.inherit_bounds;

tuned;

First version of interpretation in locales. Not yet fully functional.

Turned simp_implies into binary operator.

Added filter lemma

* Pure/Simplifier: improved handling of bound variables;

determine Poly/ML runtime system version

obsolete;

determine Poly/ML's idea of current hardware and operating system type;