# HG changeset patch
# User wenzelm
# Date 1127901013 -7200
# Node ID 8cc72452695c01f93441698c22fd67c815b1091c
# Parent  8ba7c3cd24a89173471a7fbd65b7014a295db360
revert 'defs' advertisement;
removed PG/xemacs note, which is actually wrong now;
tuned;

diff -r 8ba7c3cd24a8 -r 8cc72452695c NEWS
--- a/NEWS	Wed Sep 28 11:16:27 2005 +0200
+++ b/NEWS	Wed Sep 28 11:50:13 2005 +0200
@@ -55,11 +55,6 @@
 Classical Reasoner.  Typical big applications run around 2 times
 faster.
 
-* ProofGeneral interface: the default settings no longer prefer xemacs
-over GNU emacs.  Users typically need to experiment with various
-variations on PROOFGENERAL_OPTIONS="... -p emacs" to find the most
-stable Emacs version on their platform.
-
 
 *** Document preparation ***
 
@@ -197,17 +192,13 @@
 "logic" vs. "{}".  Potential INCOMPATIBILITY in rare cases of improper
 use of 'types'/'consts' instead of 'nonterminals'/'syntax'.  Some very
 exotic syntax specifications may require further adaption
-(e.g. Cube/Base.thy).
+(e.g. Cube/Cube.thy).
 
 * Removed obsolete type class "logic", use the top sort {} instead.
 Note that non-logical types should be declared as 'nonterminals'
 rather than 'types'.  INCOMPATIBILITY for new object-logic
 specifications.
 
-* 'defs': more well-formedness checks of overloaded definitions, but
-still does not cover all situations.  Even fails to recognize certain
-ill-formed definitions that Isabelle2004 would have rejected outright!
-
 * Attributes 'induct' and 'cases': type or set names may now be
 locally fixed variables as well.