| changeset 9224 | 0da360494917 |
| parent 9198 | 0ab3c81e9425 |
| child 9229 | a7c6ea7e57de |
--- a/NEWS Sat Jul 01 19:45:43 2000 +0200 +++ b/NEWS Sat Jul 01 19:48:04 2000 +0200 @@ -148,6 +148,10 @@ * tuned 'let' syntax: replaced 'as' keyword by 'and'; +* removed 'help' command, which hasn't been too helpful anyway; should +instead use individual commands for printing items (print_commands, +print_methods etc.); + *** HOL ***