1.1 --- a/NEWS	Sat Jul 31 21:14:20 2010 +0200
     1.2 +++ b/NEWS	Sat Jul 31 23:32:05 2010 +0200
     1.3 @@ -20,6 +20,15 @@
     1.4  files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
     1.5  
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Interpretation command 'interpret' accepts a list of equations like
    1.10 +'interpretation' does.
    1.11 +
    1.12 +* Diagnostic command 'print_interps' prints interpretations in proofs
    1.13 +in addition to interpretations in theories.
    1.14 +
    1.15 +
    1.16  *** HOL ***
    1.17  
    1.18  * code generator: export_code without explicit file declaration prints