revert 'defs' advertisement;
Wed, 28 Sep 2005 11:50:13 +0200
changeset 17691 8cc72452695c
parent 17690 8ba7c3cd24a8
child 17692 6d277e731096
revert 'defs' advertisement; removed PG/xemacs note, which is actually wrong now; tuned;
--- 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
-* 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
-* '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.