equal
deleted
inserted
replaced
31 The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance |
31 The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance |
32 readability: |
32 readability: |
33 \begin{ttbox} |
33 \begin{ttbox} |
34 Usage: expandshort [FILES|DIRS...] |
34 Usage: expandshort [FILES|DIRS...] |
35 |
35 |
36 Recursively find .ML files, expand shorthand goal commands. |
36 Recursively find .ML files, expand shorthand goal commands. Also |
37 Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
37 contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
38 rewrite_goals_tac on 1-element lists; furthermore expands tabs, |
38 forward_tac, rewrite_goals_tac on 1-element lists; furthermore expands |
39 since they are now forbidden in ML string constants. |
39 tabs, which are forbidden in SML string constants. |
40 |
40 |
41 Renames old versions of files by appending "~~". |
41 Renames old versions of files by appending "~~". |
42 \end{ttbox} |
42 \end{ttbox} |
43 In the files or directories supplied as arguments, all occurrences of |
43 In the files or directories supplied as arguments, all occurrences of |
44 the shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts |
44 the shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts |