1.1 --- a/NEWS	Tue Mar 18 22:19:18 2008 +0100
     1.2 +++ b/NEWS	Tue Mar 18 23:25:06 2008 +0100
     1.3 @@ -22,6 +22,10 @@
     1.4  conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
     1.5  provides a proper context already.
     1.6  
     1.7 +* Theory loader: old-style ML proof scripts being *attached* to a thy
     1.8 +file are no longer supported.  INCOMPATIBILITY, regular 'uses' and
     1.9 +'use' within a theory file will do the job.
    1.10 +
    1.11  
    1.12  *** Pure ***
    1.13  
    1.14 @@ -44,7 +48,7 @@
    1.15  redundant lemmas less_trans, less_linear, le_imp_less_or_eq,
    1.16  le_less_trans, less_le_trans, which merely duplicate lemmas of the
    1.17  same name in theory Orderings.  Potential INCOMPATIBILITY due to more
    1.18 -general and different variable names.
    1.19 +general types and different variable names.
    1.20  
    1.21  * Library/Option_ord.thy: Canonical order on option type.
    1.22