added undos, redos;

--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 21 12:16:41 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 21 12:17:18 1998 +0100
@@ -365,6 +365,14 @@
   OuterSyntax.parser true "redo" "redo proof command"
     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));
 
+val undosP =
+  OuterSyntax.parser true "undos" "undo proof commands"
+    (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.undos n)));
+
+val redosP =
+  OuterSyntax.parser true "redos" "redo proof commands"
+    (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.redos n)));
+
 val backP =
   OuterSyntax.parser true "back" "backtracking of proof command"
     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
@@ -501,7 +509,8 @@
   theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
   factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
   then_refineP, proofP, terminal_proofP, trivial_proofP,
-  default_proofP, clear_undoP, undoP, redoP, backP, prevP, upP, topP,
+  default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,
+  prevP, upP, topP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,

--- a/src/Pure/Isar/proof_history.ML	Sat Nov 21 12:16:41 1998 +0100
+++ b/src/Pure/Isar/proof_history.ML	Sat Nov 21 12:17:18 1998 +0100
@@ -14,6 +14,8 @@
   val clear: T -> T
   val undo: T -> T
   val redo: T -> T
+  val undos: int -> T -> T
+  val redos: int -> T -> T
   val position: T -> int
   val nesting: T -> int
   val prev: T -> T
@@ -57,6 +59,9 @@
 val undo = app History.undo;
 val redo = app History.redo;
 
+fun undos n = funpow n undo;
+fun redos n = funpow n redo;
+
 
 (* navigate *)