author | wenzelm |
Wed, 16 Jun 2004 20:36:43 +0200 | |
changeset 14954 | f1789e22ceec |
parent 14953 | 27decf8d40ff |
child 14955 | 08ee855c1d94 |
--- 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;