# HG changeset patch
# User wenzelm
# Date 962473684 -7200
# Node ID 0da3604949170d8383ab5b895972446b462f0842
# Parent  eb752c2fac22daf773d36b8705b0aa7b2d81b33f
* Isar: removed 'help' command, which hasn't been too helpful anyway;
should instead use individual commands for printing items
(print_commands, print_methods etc.);

diff -r eb752c2fac22 -r 0da360494917 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 ***