replaced rabs by overloaded abs;

yet another example

new example

tidied

better simplification of the result of simprocs

moved le_square, proved le_cube

more details

tuned msg;

val needs_filtered_use = true;

recovered \seealso;

improved indexing;

\usepackage{makeidx};

tuned GARBAGE;

improved handling of Isabelle styles (less garbage);

updated;

updated syntax of simp options: (no_asm) etc.;

removed \isabelledefaultstyle (use \isabellestyle instead);

always discgarb -c;

fixed clash with new 'abs' const;

use Sign.simple_read_term;

error msg: counting from one (again), in order to be consistent with case names of induction rule;

tuned messages; use Sign.simple_read_term;

removed dead code: listof;

use Args.colon / Args.parens;

adapted to new arithmetic simprocs;

added scan_to_id (used to be in Pure/section_utils.ML);

removed Pure/section_utils.ML;

improved syntax of method options (no_asm) etc;

removed index2;

updated;

GPLed;

GPLed;

GPLed;

GPLed; improved begin_theory: proper presentation if 'files' change theory;

GPLed; improved begin_theory ('files' may change theory);

GPLed; added colon, parens;

added simple_read_term;

tuned msg;

Added constant abs.

simprocs now simplify the RHS of their result

new lemmas about binary division

Added AVL

if_weak_cong should make linear arithmetic faster

a safer way of proving literal equalities

from Suc...Suc to #m

of course it should use Main

new lemmas concerning powers and #mmm

changed 2 to #2

Suc 0 -> 1

card_Pow is no longer a default simprule because it uses unary 2

simprocs

further tidying of integer simprocs

removed obsolete simproc combine_coeff

Installation of CombineNumerals for the integers Many bug fixes Removal of AssocFold for addition (nat and int)

removed obsolete simprocs

removed obsolete "evenness" proofs

TEMPORARY REMOVAL OF TWO BROKEN EXAMPLES

modified for new simprocs

now using binary naturals

various bug fixes