--- a/ProgTutorial/Tactical.thy	Thu Aug 13 21:32:10 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun Aug 16 21:54:47 2009 +0200
@@ -1117,6 +1117,9 @@
   definition for a constant and this constant is not present in the goal state, 
   you can still safely apply the simplifier.
 
+  (FIXME: show rewriting of cterms)
+
+
   When using the simplifier, the crucial information you have to provide is
   the simpset. If this information is not handled with care, then the
   simplifier can easily run into a loop. Therefore a good rule of thumb is to