1999-01-13 paulson 1999-01-13 removal of FOL and ZF
1999-01-13 paulson 1999-01-13 minor updates on inductive definitions and datatypes
1999-01-13 wenzelm 1999-01-13 fixed titles;
1999-01-13 paulson 1999-01-13 tidying of datatype and inductive definitions
1999-01-13 wenzelm 1999-01-13 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
1999-01-13 nipkow 1999-01-13 Refined arithmetic.
1999-01-13 paulson 1999-01-13 congruence rules finally use == instead of = and <->
1999-01-13 paulson 1999-01-13 generalized qed_spec_mp code to work for ZF
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-13 paulson 1999-01-13 better qed_spec_mp
1999-01-13 nipkow 1999-01-13 Simplified interface.
1999-01-13 nipkow 1999-01-13 Simplified arithmetic.
1999-01-12 wenzelm 1999-01-12 'same' method, 'immediate' proof;
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.