1999-01-12 wenzelm 1999-01-12 tuned msg;
1999-01-12 wenzelm 1999-01-12 SYNC;
1999-01-12 wenzelm 1999-01-12 fixed again;
1999-01-12 wenzelm 1999-01-12 improved asm_finish;
1999-01-12 wenzelm 1999-01-12 get_tthms witness theorems;
1999-01-12 nipkow 1999-01-12 Split argument structure.
1999-01-12 nipkow 1999-01-12 Restructured Arithmatic
1999-01-12 nipkow 1999-01-12 *** empty log message ***
1999-01-12 nipkow 1999-01-12 verbatim
1999-01-12 wenzelm 1999-01-12 SYNC;
1999-01-12 wenzelm 1999-01-12 fixed deriv;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1999-01-12 wenzelm 1999-01-12 tuned msg;
1999-01-12 wenzelm 1999-01-12 tuned signature;
1999-01-12 wenzelm 1999-01-12 eliminated global/local names;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1999-01-12 wenzelm 1999-01-12 eliminated Attribute structure;
1999-01-12 wenzelm 1999-01-12 signature BASIC_THM; theorem / axiom deriv: added tags; get/put_name_tags; type attribute;
1999-01-12 wenzelm 1999-01-12 fixed AUTO_PERL;
1999-01-12 wenzelm 1999-01-12 show_tags; pretty/print_thms;
1999-01-12 wenzelm 1999-01-12 added rule_attribute: ('a -> thm -> thm) -> 'a attribute; added tag / untag attributes;
1999-01-12 wenzelm 1999-01-12 Thm of string * tag list;
1999-01-12 wenzelm 1999-01-12 eliminated Attribute structure;
1999-01-12 wenzelm 1999-01-12 removed attribute.ML;
1999-01-12 wenzelm 1999-01-12 configure AUTO_BASH, AUTO_PERL;
1999-01-11 nipkow 1999-01-11 Some simplifications.
1999-01-11 nipkow 1999-01-11 More arith simplifications
1999-01-11 nipkow 1999-01-11 More arith simplifications.
1999-01-11 wenzelm 1999-01-11 more robust heap file detection;
1999-01-11 wenzelm 1999-01-11 tuned, updated;
1999-01-11 paulson 1999-01-11 tidying, e.g. from \\tt to \\texttt
1999-01-09 nipkow 1999-01-09 Remoaved a few now redundant rewrite rules.
1999-01-09 nipkow 1999-01-09 Added simproc.
1999-01-09 nipkow 1999-01-09 Refined arith tactic.
1999-01-08 paulson 1999-01-08 removal of FOL, ZF to a separate manual
1999-01-08 paulson 1999-01-08 removal of DO_GOAL
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1999-01-07 paulson 1999-01-07 if-then-else syntax for ZF
1999-01-07 paulson 1999-01-07 if-then-else syntax for ZF
1999-01-06 wenzelm 1999-01-06 fixed commit spec;
1999-01-06 nipkow 1999-01-06 Simplified proof.
1999-01-06 paulson 1999-01-06 induct_tac and exhaust_tac
1999-01-06 paulson 1999-01-06 primrec, induct_tac
1999-01-05 nipkow 1999-01-05 *** empty log message ***
1999-01-05 nipkow 1999-01-05 Small mods.
1999-01-05 nipkow 1999-01-05 1 proof now automatic.
1999-01-05 nipkow 1999-01-05 Instantiated lin.arith.
1999-01-05 nipkow 1999-01-05 In Main: moved Bin to the left to preserve the solver in its simpset.
1999-01-04 nipkow 1999-01-04 Shortened a proof.
1999-01-04 nipkow 1999-01-04 *** empty log message ***
1999-01-04 nipkow 1999-01-04 Version 1 of linear arithmetic for nat.
1999-01-04 nipkow 1999-01-04 Version 1.0 of linear nat arithmetic.
1998-12-28 paulson 1998-12-28 added new arg for print_tac
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1998-12-28 paulson 1998-12-28 revised datatype definition package
1998-12-28 paulson 1998-12-28 revised inductive definition package
1998-12-28 paulson 1998-12-28 new primrec package
1998-12-28 paulson 1998-12-28 moved from ZF to new subdirectory Tools
1998-12-28 paulson 1998-12-28 new theorem update_type