| changeset 56579 | 4c94f631c595 |
| parent 56491 | a8ccf3d6a6e4 |
| child 57421 | 94081154306d |
--- a/src/Doc/Implementation/Tactic.thy Mon Apr 14 23:26:52 2014 +0200 +++ b/src/Doc/Implementation/Tactic.thy Tue Apr 15 00:03:39 2014 +0200 @@ -431,7 +431,7 @@ \item @{ML rename_tac}~@{text "names i"} renames the innermost parameters of subgoal @{text i} according to the provided @{text - names} (which need to be distinct indentifiers). + names} (which need to be distinct identifiers). \end{description}