1999-01-12 ago wenzelm eliminated global/local names;
1999-01-12 ago wenzelm eliminated tthm type and Attribute structure;
1999-01-12 ago wenzelm eliminated tthm type and Attribute structure;
1999-01-12 ago wenzelm eliminated Attribute structure;
1999-01-12 ago wenzelm signature BASIC_THM;
1999-01-12 ago wenzelm fixed AUTO_PERL;
1999-01-12 ago wenzelm show_tags;
1999-01-12 ago wenzelm added rule_attribute: ('a -> thm -> thm) -> 'a attribute;
1999-01-12 ago wenzelm Thm of string * tag list;
1999-01-12 ago wenzelm eliminated Attribute structure;
1999-01-12 ago wenzelm removed attribute.ML;
1999-01-12 ago wenzelm configure AUTO_BASH, AUTO_PERL;
1999-01-11 ago nipkow Some simplifications.
1999-01-11 ago nipkow More arith simplifications
1999-01-11 ago nipkow More arith simplifications.
1999-01-11 ago wenzelm more robust heap file detection;
1999-01-11 ago wenzelm tuned, updated;
1999-01-11 ago paulson tidying, e.g. from \\tt to \\texttt
1999-01-09 ago nipkow Remoaved a few now redundant rewrite rules.
1999-01-09 ago nipkow Added simproc.
1999-01-09 ago nipkow Refined arith tactic.
1999-01-08 ago paulson removal of FOL, ZF to a separate manual
1999-01-08 ago paulson removal of DO_GOAL
1999-01-07 ago paulson ZF: the natural numbers as a datatype
1999-01-07 ago paulson if-then-else syntax for ZF
1999-01-07 ago paulson if-then-else syntax for ZF
1999-01-06 ago wenzelm fixed commit spec;
1999-01-06 ago nipkow Simplified proof.
1999-01-06 ago paulson induct_tac and exhaust_tac
1999-01-06 ago paulson primrec, induct_tac
1999-01-05 ago nipkow *** empty log message ***
1999-01-05 ago nipkow Small mods.
1999-01-05 ago nipkow 1 proof now automatic.
1999-01-05 ago nipkow Instantiated lin.arith.
1999-01-05 ago nipkow In Main: moved Bin to the left to preserve the solver in its simpset.
1999-01-04 ago nipkow Shortened a proof.
1999-01-04 ago nipkow *** empty log message ***
1999-01-04 ago nipkow Version 1 of linear arithmetic for nat.
1999-01-04 ago nipkow Version 1.0 of linear nat arithmetic.
1998-12-28 ago paulson added new arg for print_tac
1998-12-28 ago paulson new inductive, datatype and primrec packages, etc.
1998-12-28 ago paulson revised datatype definition package
1998-12-28 ago paulson revised inductive definition package
1998-12-28 ago paulson new primrec package
1998-12-28 ago paulson moved from ZF to new subdirectory Tools
1998-12-28 ago paulson new theorem update_type
1998-12-28 ago paulson converted to use new primrec section and update operator
1998-12-28 ago paulson converted to use new primrec section
1998-12-28 ago paulson fixed comment
1998-12-28 ago paulson Needs separate theory Primrec_defs due to new inductive defs package
1998-12-28 ago paulson more efficient strip_quotes using "substring"
1998-12-28 ago paulson Basis Library compatible substring oeration
1998-12-28 ago paulson Added a "message" argument to print_tac
1998-12-28 ago paulson comments
1998-12-28 ago paulson deleted "escape" and "trim"; Basis Library can do string escapes if necessary
1998-12-28 ago paulson String added to BasisLibrary
1998-12-28 ago paulson better indentation
1998-12-28 ago paulson fixed comments
1998-12-28 ago paulson replaced obsolete "trim" by "strip_quotes"
1998-12-18 ago nipkow Link to HOLCF paper added.