src/Pure/Isar/isar_syn.ML
changeset 5991 832ec852fc4e
parent 5958 c48efb523a4d
child 6013 6da9ae6d40f5
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 29 13:17:21 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 29 13:17:42 1998 +0100
@@ -490,6 +490,10 @@
   OuterSyntax.parser true "exit" "exit Isar loop"
     (Scan.succeed IsarCmd.exit);
 
+val restartP =
+  OuterSyntax.parser true "restart" "restart Isar loop"
+    (Scan.succeed IsarCmd.restart);
+
 val breakP =
   OuterSyntax.parser true "break" "discontinue excursion (keep current state)"
     (Scan.succeed IsarCmd.break);
@@ -528,7 +532,7 @@
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)
-  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];
+  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, restartP, breakP];
 
 
 end;