diff -r 5dcee4d751ad -r 0b337dedc306 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Thu Nov 12 20:35:14 2009 +0100 +++ b/ProgTutorial/Tactical.thy Sun Nov 15 13:18:07 2009 +0100 @@ -1314,7 +1314,7 @@ \end{exercise} *} -section {* Simplifier Tactics *} +section {* Simplifier Tactics\label{sec:simplifier} *} text {* A lot of convenience in reasoning with Isabelle derives from its