diff -r 576a7f5e5e39 -r dcc446da8e19 src/Pure/Isar/proof_history.ML
--- 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 *)