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
1998-12-28 paulson 1998-12-28 converted to use new primrec section and update operator
1998-12-28 paulson 1998-12-28 converted to use new primrec section
1998-12-28 paulson 1998-12-28 fixed comment
1998-12-28 paulson 1998-12-28 Needs separate theory Primrec_defs due to new inductive defs package
1998-12-28 paulson 1998-12-28 more efficient strip_quotes using "substring"
1998-12-28 paulson 1998-12-28 Basis Library compatible substring oeration
1998-12-28 paulson 1998-12-28 Added a "message" argument to print_tac
1998-12-28 paulson 1998-12-28 comments
1998-12-28 paulson 1998-12-28 deleted "escape" and "trim"; Basis Library can do string escapes if necessary
1998-12-28 paulson 1998-12-28 String added to BasisLibrary
1998-12-28 paulson 1998-12-28 better indentation
1998-12-28 paulson 1998-12-28 fixed comments
1998-12-28 paulson 1998-12-28 replaced obsolete "trim" by "strip_quotes"
1998-12-18 nipkow 1998-12-18 Link to HOLCF paper added.
1998-12-18 paulson 1998-12-18 moved dest_Type to term.ML from HOL/Tools/primrec_package
1998-12-18 paulson 1998-12-18 moved dest_eq to hologic.ML and tidied
1998-12-18 paulson 1998-12-18 new function dest_eq
1998-12-17 wenzelm 1998-12-17 tuned mode_name;
1998-12-17 wenzelm 1998-12-17 bash -c :;
1998-12-11 oheimb 1998-12-11 *** empty log message ***
1998-12-11 oheimb 1998-12-11 added new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows)
1998-12-11 oheimb 1998-12-11 better representation of Sigma
1998-12-11 oheimb 1998-12-11 initisaterm now obsolete changed modifiers
1998-12-11 paulson 1998-12-11 new Close_locale synatx
1998-12-11 paulson 1998-12-11 deleted unclosed comment
1998-12-11 paulson 1998-12-11 the + facility for locales, by Florian
1998-12-11 paulson 1998-12-11 new Close_locale synatx
1998-12-07 paulson 1998-12-07 towards handling sharing of variables
1998-12-07 paulson 1998-12-07 tidying
1998-12-07 paulson 1998-12-07 expandshort