changeset 14954 | f1789e22ceec |
parent 14925 | 0f86a8a694f8 |
child 14981 | e73f8140af78 |
--- a/src/Pure/Isar/outer_syntax.ML Wed Jun 16 14:56:58 2004 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Wed Jun 16 20:36:43 2004 +0200 @@ -388,13 +388,6 @@ fun sync_loop () = gen_loop true true; -(* help *) - -fun help () = - writeln ("This is Isabelle's underlying ML system (" ^ ml_system ^ ");\n\ - \invoke 'Isar.loop();' to get back to the Isar read-eval-print loop."); - - (*final declarations of this structure!*) val command = parser false None; val markup_command = parser false o Some;