tuned;
authorwenzelm
Sat Mar 18 19:16:56 2000 +0100 (2000-03-18)
changeset 8518daaedc7b56a9
parent 8517 062e6cd78534
child 8519 981f52707e5d
tuned;
NEWS
     1.1 --- a/NEWS	Sat Mar 18 19:11:34 2000 +0100
     1.2 +++ b/NEWS	Sat Mar 18 19:16:56 2000 +0100
     1.3 @@ -9,30 +9,30 @@
     1.4  
     1.5  * HOL: the constant for f``x is now "image" rather than "op ``".
     1.6  
     1.7 -* HOL: exhaust_tac on datatypes superceded by new case_tac;
     1.8 +* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
     1.9  
    1.10 -* ML: PureThy.add_thms/add_axioms/add_defs now return theorems;
    1.11 +* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.12  
    1.13  
    1.14  *** Document preparation ***
    1.15  
    1.16  * isatool mkdir provides easy setup of Isabelle session directories,
    1.17 -including proper documents;
    1.18 +including proper document sources;
    1.19  
    1.20  * generated LaTeX sources are now deleted after successful run
    1.21  (isatool document -c); may retain a copy somewhere else via -D option
    1.22  of isatool usedir;
    1.23  
    1.24 -* old-style theories now produce (crude) LaTeX sources as well;
    1.25 +* old-style theories now produce (crude) LaTeX output as well;
    1.26  
    1.27  
    1.28  *** Isar ***
    1.29  
    1.30  * Pure now provides its own version of intro/elim/dest attributes;
    1.31  useful for building new logics, but beware of confusion with the
    1.32 -Provers/classical ones!
    1.33 +Provers/classical ones;
    1.34  
    1.35 -* Pure: new 'obtain' language element supports generalized existence
    1.36 +* Pure: new 'obtain' language element supports generalized elimination
    1.37  proofs;
    1.38  
    1.39  * Pure: scalable support for case-analysis type proofs: new 'case'
    1.40 @@ -53,19 +53,19 @@
    1.41  
    1.42  * names of theorems etc. may be natural numbers as well;
    1.43  
    1.44 -* intro/elim/dest attributes: changed ! / !! flags to ? / ??;
    1.45 +* Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;
    1.46  
    1.47  * 'pr' command: optional goals_limit argument;
    1.48  
    1.49  * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
    1.50 -additional print modes to be specified; e.g. pr(latex) will print
    1.51 -proof according to the Isabelle LaTeX style;
    1.52 +additional print modes to be specified; e.g. "pr(latex)" will print
    1.53 +proof state according to the Isabelle LaTeX style;
    1.54  
    1.55  
    1.56  *** HOL ***
    1.57  
    1.58 -* Algebra: new theory of rings and univariate polynomials, by Clemens
    1.59 -Ballarin;
    1.60 +* HOL/Algebra: new theory of rings and univariate polynomials, by
    1.61 +Clemens Ballarin;
    1.62  
    1.63  * HOL/record: fixed select-update simplification procedure to handle
    1.64  extended records as well; admit "r" as field name;
    1.65 @@ -75,18 +75,16 @@
    1.66  
    1.67  * new version of "case_tac" subsumes both boolean case split and
    1.68  "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
    1.69 -exists, may define val exhaust_tac = case_tac for quick-and-dirty
    1.70 -portability;
    1.71 +exists, may define val exhaust_tac = case_tac for ad-hoc portability;
    1.72  
    1.73  
    1.74  *** General ***
    1.75  
    1.76  * compression of ML heaps images may now be controlled via -c option
    1.77 -of isabelle and isatool usedir;
    1.78 +of isabelle and isatool usedir (currently only observed by Poly/ML);
    1.79  
    1.80 -* new ML combinators |>> and |>>> for incremental transformations with
    1.81 -secondary results (e.g. certain theory extensions):
    1.82 -
    1.83 +* ML: new combinators |>> and |>>> for incremental transformations
    1.84 +with secondary results (e.g. certain theory extensions):
    1.85  
    1.86  
    1.87