changed to cope with the rewriting of #2+n to Suc(Suc n)

new policy to simplify the use of numerals: #0 -> 0 #1 -> 1 #2 + n -> Suc (Suc n) similarly for n + #2

reverted to old proof of dominoes_tile_row, given new treatment of #2+...

Replaced some definitions involving epsilon by more readable primrec definitions.

alist_rec and assoc are now defined using primrec and thus no longer refer to the recursion combinator list_rec, which should be considered internal.

Removed unnecessary primrec equations of hd and last involving arbitrary.

collected three proofs into rename_client_map_tac

added the dummy theory Integ/NatSimprocs.thy

updated

new simprules needed because of new subtraction rewriting

nat_diff_split' now called nat_diff_split

deleted a lot of obsolete arithmetic lemmas

tidied

new simprules for nat_case and nat_rec simplify_meta_eq now maps #0 to 0 and #1 to 1 in its result

tidying, especially to remove zcompare_rls from proofs

a massive tidy-up

NatSimprocs is now a theory, not a file

new theorem one_le_power

tidied

deleted some redundant simprules Added new simprules for subtraction

new dummy theory; prevents strange errors when loading NatSimprocs.ML

improved name of simproc;

fixed theory deps;

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;