diff -r 06fd1914b902 -r 2c1913d1b945 NEWS --- a/NEWS Sat Jul 31 21:14:20 2010 +0200 +++ b/NEWS Sat Jul 31 23:32:05 2010 +0200 @@ -20,6 +20,15 @@ files exclusively use the .ML extension. Minor INCOMPATIBILTY. +*** Pure *** + +* Interpretation command 'interpret' accepts a list of equations like +'interpretation' does. + +* Diagnostic command 'print_interps' prints interpretations in proofs +in addition to interpretations in theories. + + *** HOL *** * code generator: export_code without explicit file declaration prints