src/Pure/Isar/outer_syntax.ML
changeset 14954 f1789e22ceec
parent 14925 0f86a8a694f8
child 14981 e73f8140af78
     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;