modified less/less_eq syntax to avoid "x < y < z" etc.;

added lemma mult_mono'

added LIM_norm and related lemmas

moved theories Parity, GCD, Binomial to Library;

added profiling code, improved handling of proof terms, generation of domain introduction rules becomes optional (global reference FundefCommon.domintros)

incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;

case_tr': proper handling of authentic consts;

removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);

renamed DatatypeHooks.invoke to all

moved lemma eq_neq_eq_imp_neq to HOL

renamed Lattice_Locales to Lattices

abstract ordering theories

obsolete (cf. ROOT.ML);

added structure Main (from Main.ML);

proper definition of add_zero_left/right;

removed NatArith.thy, Main.ML;

removed theory NatArith (now part of Nat);

* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".

moved contribution note to CONTRIBUTORS;

Made "termination by lexicographic_order" the default for "fun" definitions.

LIM_compose -> isCont_LIM_compose; cleaned up and reorganized sections

generalized types of of_nat and of_int to work with non-commutative types

untabified

complex goal statements: misc cleanup;

Added datatype hook to declare all case_congs as "fundef_cong" automatically.

removed obsolete theorem statements (cf. specification.ML);

tuned specifications;

fixed locale fact references;

removed obsolete print_state_hook;

theorem statements: incorporate Obtain.statement, tuned;