--- a/ProgTutorial/Tactical.thy	Wed Aug 19 00:49:40 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Aug 19 09:25:49 2009 +0200
@@ -14,7 +14,6 @@
   steps until all of them are solved. However, there are also more structured
   operations available on the ML-level that help with the handling of
   variables and assumptions.
-
 *}
 
 
@@ -1067,6 +1066,10 @@
   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
   \end{readmore}
 
+  \begin{exercise}\label{ex:dyckhoff}
+  
+  \end{exercise}
+
 *}
 
 section {* Simplifier Tactics *}