*** empty log message ***
authornipkow
Mon Aug 16 14:21:54 2004 +0200 (2004-08-16)
changeset 15130dc6be28d7f4e
parent 15129 fbf90acc5bf4
child 15131 c69542757a4d
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Mon Aug 16 12:29:09 2004 +0200
     1.2 +++ b/NEWS	Mon Aug 16 14:21:54 2004 +0200
     1.3 @@ -6,6 +6,19 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Theory headers: the new header syntax for Isar theories is
     1.8 +
     1.9 +  theory <name>
    1.10 +  import <theory1> ... <theoryn>
    1.11 +  begin
    1.12 +
    1.13 +  optionally also with a "files" section. The old syntax
    1.14 +
    1.15 +  theory <name> = <theory1> + ... + <theoryn>:
    1.16 +
    1.17 +  will still be supported for some time but will eventually disappear.
    1.18 +  The syntax of old-style theories has not changed.
    1.19 +
    1.20  * Provers/quasi.ML:  new transitivity reasoners for transitivity only
    1.21    and quasi orders.
    1.22