base on IntArith instead of Int (in order to leave out deleted simproc!);

dest_mss: sort procs wrt. names;

FAKE_BUILD;

polyml;

tuned;

new default simprule for better compatibility with old setup

tidied

tuned;

use proper version of pdfsetup.sty;

added semicolons;

updated keywords;

named "op ^" definitions;

improved X-Symbol stuff;

more examples

added INSTALL;

moved theory Sexp to Induct examples;

strip = impI allI allI;

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

Cassini identity is easier to prove using INTEGERS

a more modern proof

now with combine_numerals

combine_numerals replaces both fold_Suc and combine_coeff

new simproc, replacing combine_coeffs and working for nat, int, real

signature change

inserted triviality check

*** empty log message ***

new, but still slow, proofs using binary numerals

[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist

number_of now takes a type arg

this change saves 15 seconds

bug fixes to new simprocs

[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist

removed some duplication, etc.

now uses the new cancel_numerals simproc

Provers/Arith/inverse_fold.ML is already obsolete

cleaner exceptions

now works for coefficients, not just for numerals no longer works by subtraction, so no need for inverse_fold

new file containing simproc invocations, from NatBin.ML

moved the simproc code to NatSimprocs.ML

Provers/Arith/inverse_fold.ML is already obsolete

new file Integ/NatSimprocs.ML

Provers/Arith/inverse_fold.ML is already obsolete Integ/NatSimprocs.ML added

*** empty log message ***

*** empty log message ***

TuturialI;

*** empty log message ***

check_file: keep expanded (!) absolute path;

Adding generated files

*** empty log message ***

fixed -c default value;

Adding generated files.

I wonder which files i forgot.

*** empty log message ***

I wonder if that's all?

deleted obsolete lemma_not_leI2

removal of less_SucI, le_SucI from default simpset

replaced obsolete diff_right_cancel by diff_diff_eq

added number_of_const: term

tidied

instantiates new simprocs for numerals of type "nat"

new simprocs for numerals of type "nat"