src/Pure/Isar/proof_history.ML

   val init: Proof.state -> T
   val current: T -> Proof.state
   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
   val up: T -> T
   val top: T -> T

 fun init st = ProofHistory (History.init (((st, Seq.empty), 0), []));
 fun current (ProofHistory prf) = fst (fst (fst (History.current prf)));
 val clear = app History.clear;
 val undo = app History.undo;
 val redo = app History.redo;
+
+fun undos n = funpow n undo;
+fun redos n = funpow n redo;
 
 
 (* navigate *)
 
 fun position (ProofHistory prf) = length (snd (History.current prf));