src/Pure/Isar/outer_syntax.ML
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;