| changeset 39847 | da8c3fc5e314 |
| parent 34930 | f3bce1cc513c |
| child 39852 | 9c977f899ebf |
--- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Oct 13 13:05:23 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Oct 13 21:57:21 2010 +0100 @@ -86,7 +86,7 @@ *} -section {* Tactics *} +section {* Tactics\label{sec:tactics} *} text {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that maps a given goal state (represented as a theorem, cf.\