removed unused help function;
authorwenzelm
Wed Jun 16 20:36:43 2004 +0200 (2004-06-16)
changeset 14954f1789e22ceec
parent 14953 27decf8d40ff
child 14955 08ee855c1d94
removed unused help function;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jun 16 14:56:58 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Jun 16 20:36:43 2004 +0200
     1.3 @@ -388,13 +388,6 @@
     1.4  fun sync_loop () = gen_loop true true;
     1.5  
     1.6  
     1.7 -(* help *)
     1.8 -
     1.9 -fun help () =
    1.10 -  writeln ("This is Isabelle's underlying ML system (" ^ ml_system ^ ");\n\
    1.11 -    \invoke 'Isar.loop();' to get back to the Isar read-eval-print loop.");
    1.12 -
    1.13 -
    1.14  (*final declarations of this structure!*)
    1.15  val command = parser false None;
    1.16  val markup_command = parser false o Some;