| changeset 40126 | 916cb4a28ffd |
| parent 39864 | f3b4fde34cd1 |
| child 40255 | 9ffbc25e1606 |
--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Oct 25 11:39:52 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Oct 25 16:14:40 2010 +0200 @@ -784,7 +784,7 @@ *} -subsection {* Auxiliary definitions *} +subsection {* Auxiliary definitions \label{sec:logic-aux} *} text {* Theory @{text "Pure"} provides a few auxiliary definitions, see