NEWS
changeset 38110 2c1913d1b945
parent 37939 965537d86fcc
child 38135 2b9bfa0b44f1
--- 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