# HG changeset patch
# User wenzelm
# Date 955973553 -7200
# Node ID 094dbd0fad0c3035fd11c1f31094e62b3c56e0cf
# Parent  33a9643ba62602bbb4772dfbece0f5fa4c513e4c
* improved name spaces: ambiguous output is qualified; support for
hiding of names;

diff -r 33a9643ba626 -r 094dbd0fad0c NEWS
--- 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