changeset 388 | 0b337dedc306 |
parent 384 | 0b24a016f6dd |
child 401 | 36d61044f9bf |
--- 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