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;

moved statement to specification.ML;

removed obsolete Locale.smart_theorem;

avoid handling of arbitrary exceptions;

field-update in records is generalised to take a function on the field rather than the new value.

exported intro_locales_tac ----------------------------------------------------------------------

Proper theorem names at last, no fakes!! Added set_prover function to set various parameters to improve success rate. Fixed the auto settings for E.

some corrections

adjusted title

simplified dest_eq; do not export debuging stuff; has_tvars: actually check all types within a term, not just its resulting type; tuned;

commented out parts which have been inactive (unintentionally) for a long time;

removed obsolete dest_eq_typ;

tuned hypsubst setup;