--- a/ProgTutorial/Tactical.thy	Sat Nov 07 10:08:09 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Mon Nov 09 09:25:51 2009 +0100
@@ -1806,14 +1806,13 @@
 lemma 
   shows "Suc 0 = 1"
 apply(simp)
-(*<*)oops(*>*)
-
-text {*
-  \begin{isabelle}
+txt{*
+  \begin{minipage}{\textwidth}
+  \small@{text "> The redex: Suc 0"}\\
   @{text "> The redex: Suc 0"}\\
-  @{text "> The redex: Suc 0"}\\
-  \end{isabelle}
-
+  \end{minipage}*}(*<*)oops(*>*)
+
+text {* 
   This will print out the message twice: once for the left-hand side and
   once for the right-hand side. The reason is that during simplification the
   simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc