--- a/NEWS Mon Aug 16 12:29:09 2004 +0200
+++ b/NEWS Mon Aug 16 14:21:54 2004 +0200
@@ -6,6 +6,19 @@
*** General ***
+* Theory headers: the new header syntax for Isar theories is
+
+ theory <name>
+ import <theory1> ... <theoryn>
+ begin
+
+ optionally also with a "files" section. The old syntax
+
+ theory <name> = <theory1> + ... + <theoryn>:
+
+ will still be supported for some time but will eventually disappear.
+ The syntax of old-style theories has not changed.
+
* Provers/quasi.ML: new transitivity reasoners for transitivity only
and quasi orders.