ProgTutorial/Tactical.thy
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