# HG changeset patch
# User wenzelm
# Date 1129751550 -7200
# Node ID 93e26302733e33544171bb2f4bb339f1186ebb17
# Parent  3c6e7760da896a7cf045791f101d2f46f49621a2
* Theory syntax: discontinued non-Isar format and old Isar headers;

diff -r 3c6e7760da89 -r 93e26302733e NEWS
--- a/NEWS	Wed Oct 19 21:52:29 2005 +0200
+++ b/NEWS	Wed Oct 19 21:52:30 2005 +0200
@@ -6,6 +6,19 @@
 
 *** General ***
 
+* Theory syntax: the header format ``theory A = B + C:'' has been
+discontinued in favour of ``theory A imports B C begin''.  Use isatool
+fixheaders to convert existing theory files.  INCOMPATIBILITY.
+
+* Theory syntax: the old non-Isar theory file format has been
+discontinued altogether.  Note that ML proof scripts may still be used
+with Isar theories; migration is usually quite simple with the ML
+function use_legacy_bindings.  INCOMPATIBILITY.
+
+* Legacy goal package: removed former user-level functions top_sg,
+prin, printyp, pprint_term/typ, which tend to cause confusion about
+the actual goal (!) context being used here.
+
 * Command 'find_theorems': support "*" wildcard in "name:" criterion.