* Isar: removed 'help' command, which hasn't been too helpful anyway;
authorwenzelm
Sat, 01 Jul 2000 19:48:04 +0200
changeset 9224 0da360494917
parent 9223 eb752c2fac22
child 9225 4772656ddbbc
* Isar: removed 'help' command, which hasn't been too helpful anyway; should instead use individual commands for printing items (print_commands, print_methods etc.);
NEWS
--- 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 ***