Merge commit 'dae42fb8b56113af92d1fc5b186acd79490a02eb' into probabil…

…ity_dev

Manual/Description/libraries.stex

@@ -1289,10 +1289,12 @@ The abbreviation \ml{e} may also be used to expand a tactic.
 \begin{hol}
 \begin{verbatim}
    b          : unit -> goalstack
+   rd         : unit -> goalstack
    drop       : unit -> proofs
    dropn      : int  -> proofs
    drop_all   : unit -> proofs
    backup     : unit -> goalstack
+   redo       : unit -> goalstack
    restart    : unit -> goalstack
    set_backup : int  -> unit
 \end{verbatim}
@@ -1302,7 +1304,8 @@ Often (we are tempted to say {\it usually}!) one takes a wrong path
 in doing a proof, or makes a mistake when setting a goal. To undo a step
 in the goalstack, the function \ml{backup} and its abbreviation
 \ml{b} are used. This will restore the goalstack to its previous
-state.
+state. To redo a step in the goalstack, the \ml{redo} function,
+abbreviated as \ml{rd}, may be used.
 
 
 To directly back up all the way to the original goal, the function

Manual/Translations/IT/Description/libraries.tex

@@ -1283,9 +1283,11 @@ \subsection{Undo}
 \begin{hol}
 \begin{verbatim}
    b          : unit -> goalstack
+   rd         : unit -> goalstack
    drop       : unit -> proofs
    dropn      : int  -> proofs
    backup     : unit -> goalstack
+   redo       : unit -> goalstack
    restart    : unit -> goalstack
    set_backup : int  -> unit
 \end{verbatim}
@@ -1294,8 +1296,9 @@ \subsection{Undo}
 Spesso (siamo tentati di dire {\it di solito}!) si prende una strada sbagliata
 nel fare una dimostrazione, o si fa un errore nell'impostare un goal. Per annullare un passo
 nel goalstack, sono usate la funzione \ml{backup} e la sua abbreviazione
-\ml{b}. Questo ripristinerà il goalstack al suo stato
-precedente.
+\ml{b}. Questo ripristinerà il goalstack al suo stato precedente.
+Per rifare un passaggio nel goalstack, si usa la funzione \ml{redo},
+abbreviata come \ml{rd}.
 
 
 Per eseguire il backup completo al goal originale, può essere usata