* improved name spaces: ambiguous output is qualified; support for
authorwenzelm
Mon Apr 17 14:12:33 2000 +0200 (2000-04-17)
changeset 8729094dbd0fad0c
parent 8728 33a9643ba626
child 8730 d97ee7249698
* improved name spaces: ambiguous output is qualified; support for
hiding of names;
NEWS
     1.1 --- a/NEWS	Mon Apr 17 14:10:38 2000 +0200
     1.2 +++ b/NEWS	Mon Apr 17 14:12:33 2000 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -6,10 +7,10 @@
     1.9  
    1.10  *** Overview of INCOMPATIBILITIES (see below for more details) ***
    1.11  
    1.12 -* HOL: the constant for f``x is now "image" rather than "op ``".
    1.13 +* HOL: the constant for f``x is now "image" rather than "op ``";
    1.14  
    1.15 -* HOL: the cartesian product is now "<*>" instead of "Times".
    1.16 -       the lexicographic product is now "<*lex*>" instead of "**".
    1.17 +* HOL: the cartesian product is now "<*>" instead of "Times"; the
    1.18 +lexicographic product is now "<*lex*>" instead of "**";
    1.19  
    1.20  * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
    1.21  
    1.22 @@ -20,6 +21,8 @@
    1.23  
    1.24  * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.25  
    1.26 +* LaTeX: several improvements of isabelle.sty;
    1.27 +
    1.28  
    1.29  *** Document preparation ***
    1.30  
    1.31 @@ -88,6 +91,9 @@
    1.32  
    1.33  * tuned 'let' syntax: replace 'as' keyword by 'and';
    1.34  
    1.35 +* theory command 'hide' removes declarations from class/type/const
    1.36 +name spaces;
    1.37 +
    1.38  
    1.39  *** HOL ***
    1.40  
    1.41 @@ -123,6 +129,9 @@
    1.42  
    1.43  *** General ***
    1.44  
    1.45 +* improved name spaces: ambiguous output is qualified; support for
    1.46 +hiding of names;
    1.47 +
    1.48  * compression of ML heaps images may now be controlled via -c option
    1.49  of isabelle and isatool usedir (currently only observed by Poly/ML);
    1.50  
    1.51 @@ -163,10 +172,10 @@
    1.52  * HOL/List: the constructors of type list are now Nil and Cons;
    1.53  
    1.54  * Simplifier: the type of the infix ML functions
    1.55 -	setSSolver addSSolver setSolver addSolver
    1.56 +        setSSolver addSSolver setSolver addSolver
    1.57  is now  simpset * solver -> simpset  where `solver' is a new abstract type
    1.58  for packaging solvers. A solver is created via
    1.59 -	mk_solver: string -> (thm list -> int -> tactic) -> solver
    1.60 +        mk_solver: string -> (thm list -> int -> tactic) -> solver
    1.61  where the string argument is only a comment.
    1.62  
    1.63  
    1.64 @@ -386,7 +395,7 @@
    1.65  
    1.66  * the simplifier is now installed
    1.67  
    1.68 -* the axiom system has been generalized (thanks to Soren Heilmann) 
    1.69 +* the axiom system has been generalized (thanks to Soren Heilmann)
    1.70  
    1.71  * the classical reasoner now has a default rule database
    1.72