# HG changeset patch
# User nipkow
# Date 1092658914 -7200
# Node ID dc6be28d7f4ee4ac053d9f3a8811739ea7a89fbd
# Parent  fbf90acc5bf4b1fe2fc2e17ccb1541dbecdd3d9c
*** empty log message ***

diff -r fbf90acc5bf4 -r dc6be28d7f4e NEWS
--- 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.