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

author | wenzelm |

Mon, 17 Apr 2000 14:12:33 +0200 | |

changeset 8729 | 094dbd0fad0c |

parent 8728 | 33a9643ba626 |

child 8730 | d97ee7249698 |

* improved name spaces: ambiguous output is qualified; support for
hiding of names;

--- a/NEWS Mon Apr 17 14:10:38 2000 +0200 +++ b/NEWS Mon Apr 17 14:12:33 2000 +0200 @@ -1,3 +1,4 @@ + Isabelle NEWS -- history user-relevant changes ============================================== @@ -6,10 +7,10 @@ *** Overview of INCOMPATIBILITIES (see below for more details) *** -* HOL: the constant for f``x is now "image" rather than "op ``". +* HOL: the constant for f``x is now "image" rather than "op ``"; -* HOL: the cartesian product is now "<*>" instead of "Times". - the lexicographic product is now "<*lex*>" instead of "**". +* HOL: the cartesian product is now "<*>" instead of "Times"; the +lexicographic product is now "<*lex*>" instead of "**"; * HOL: exhaust_tac on datatypes superceded by new generic case_tac; @@ -20,6 +21,8 @@ * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; +* LaTeX: several improvements of isabelle.sty; + *** Document preparation *** @@ -88,6 +91,9 @@ * tuned 'let' syntax: replace 'as' keyword by 'and'; +* theory command 'hide' removes declarations from class/type/const +name spaces; + *** HOL *** @@ -123,6 +129,9 @@ *** General *** +* improved name spaces: ambiguous output is qualified; support for +hiding of names; + * compression of ML heaps images may now be controlled via -c option of isabelle and isatool usedir (currently only observed by Poly/ML); @@ -163,10 +172,10 @@ * HOL/List: the constructors of type list are now Nil and Cons; * Simplifier: the type of the infix ML functions - setSSolver addSSolver setSolver addSolver + setSSolver addSSolver setSolver addSolver is now simpset * solver -> simpset where `solver' is a new abstract type for packaging solvers. A solver is created via - mk_solver: string -> (thm list -> int -> tactic) -> solver + mk_solver: string -> (thm list -> int -> tactic) -> solver where the string argument is only a comment. @@ -386,7 +395,7 @@ * the simplifier is now installed -* the axiom system has been generalized (thanks to Soren Heilmann) +* the axiom system has been generalized (thanks to Soren Heilmann) * the classical reasoner now has a default rule database