src/Pure/Isar/isar_syn.ML
changeset 7462 f738df1d82e1
parent 7415 bd819d0255e1
child 7603 b2b5599b934f
--- a/src/Pure/Isar/isar_syn.ML	Fri Sep 03 18:16:54 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Sep 03 18:17:51 1999 +0200
@@ -559,6 +559,10 @@
   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
     (Scan.succeed IsarCmd.init_toplevel);
 
+val welcomeP =
+  OuterSyntax.improper_command "welcome" "print welcome message" K.control
+    (Scan.succeed IsarCmd.welcome);
+
 
 
 (** the Pure outer syntax **)
@@ -599,7 +603,7 @@
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,
-  enable_prP, commitP, quitP, exitP, init_toplevelP];
+  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
 
 
 end;