summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 18 Mar 2000 19:16:56 +0100 | |

changeset 8518 | daaedc7b56a9 |

parent 8517 | 062e6cd78534 |

child 8519 | 981f52707e5d |

tuned;

--- a/NEWS Sat Mar 18 19:11:34 2000 +0100 +++ b/NEWS Sat Mar 18 19:16:56 2000 +0100 @@ -9,30 +9,30 @@ * HOL: the constant for f``x is now "image" rather than "op ``". -* HOL: exhaust_tac on datatypes superceded by new case_tac; +* HOL: exhaust_tac on datatypes superceded by new generic case_tac; -* ML: PureThy.add_thms/add_axioms/add_defs now return theorems; +* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; *** Document preparation *** * isatool mkdir provides easy setup of Isabelle session directories, -including proper documents; +including proper document sources; * generated LaTeX sources are now deleted after successful run (isatool document -c); may retain a copy somewhere else via -D option of isatool usedir; -* old-style theories now produce (crude) LaTeX sources as well; +* old-style theories now produce (crude) LaTeX output as well; *** Isar *** * Pure now provides its own version of intro/elim/dest attributes; useful for building new logics, but beware of confusion with the -Provers/classical ones! +Provers/classical ones; -* Pure: new 'obtain' language element supports generalized existence +* Pure: new 'obtain' language element supports generalized elimination proofs; * Pure: scalable support for case-analysis type proofs: new 'case' @@ -53,19 +53,19 @@ * names of theorems etc. may be natural numbers as well; -* intro/elim/dest attributes: changed ! / !! flags to ? / ??; +* Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??; * 'pr' command: optional goals_limit argument; * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit -additional print modes to be specified; e.g. pr(latex) will print -proof according to the Isabelle LaTeX style; +additional print modes to be specified; e.g. "pr(latex)" will print +proof state according to the Isabelle LaTeX style; *** HOL *** -* Algebra: new theory of rings and univariate polynomials, by Clemens -Ballarin; +* HOL/Algebra: new theory of rings and univariate polynomials, by +Clemens Ballarin; * HOL/record: fixed select-update simplification procedure to handle extended records as well; admit "r" as field name; @@ -75,18 +75,16 @@ * new version of "case_tac" subsumes both boolean case split and "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer -exists, may define val exhaust_tac = case_tac for quick-and-dirty -portability; +exists, may define val exhaust_tac = case_tac for ad-hoc portability; *** General *** * compression of ML heaps images may now be controlled via -c option -of isabelle and isatool usedir; +of isabelle and isatool usedir (currently only observed by Poly/ML); -* new ML combinators |>> and |>>> for incremental transformations with -secondary results (e.g. certain theory extensions): - +* ML: new combinators |>> and |>>> for incremental transformations +with secondary results (e.g. certain theory extensions):