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