changeset 5944 | dcc446da8e19 |
parent 5827 | 77071ac7c7b5 |
child 6374 | a67e4729efb2 |
--- 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 *)