diff -r e91f54791e14 -r 007e09485351 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Sep 09 14:57:23 2008 +0200
+++ b/CookBook/FirstSteps.thy	Tue Sep 16 00:43:45 2008 +0200
@@ -26,18 +26,20 @@
 
 
 text {* 
-  Isabelle programming is done Standard ML, however it often uses an 
-  antiquotation mehanism  to refer to the logical context of Isabelle.
-  The ML-code that one writes is, just like lemmas and proofs in Isabelle, 
-  part of a theory. If you want to follow the code written in this
-  chapter, we assume you are working inside the theory defined as
+  Isabelle programming is done in Standard ML, however ML-code for Isabelle often
+  includes antiquotations to refer to the logical context of Isabelle. 
+  Just like lemmas and proofs, code in Isabelle is part of a 
+  theory. If you want to follow the code written in this chapter, we 
+  assume you are working inside the theory defined by
 
+  \begin{center}
   \begin{tabular}{@ {}l}
   \isacommand{theory} CookBook\\
   \isacommand{imports} Main\\
   \isacommand{begin}\\
+  \ldots
   \end{tabular}
-
+  \end{center}
 
   The easiest and quickest way to include code in a theory is
   by using the \isacommand{ML} command. For example
@@ -48,11 +50,11 @@
 *}
 
 text {*
-  The expression inside \isacommand{ML} commands is emmediately evaluated
-  like ``normal'' proof scripts by using the advance and retreat buttons of 
+  The expression inside \isacommand{ML} commands is immediately evaluated,
+  like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
   your Isabelle environment. The code inside the \isacommand{ML} command 
-  can also contain value- and function bindings. \marginpar{\tiny FIXME can one undo them like 
-  Isabelle lemmas/proofs - probably not}
+  can also contain value- and function bindings, on which the undo operation 
+  does not have any effect. 
 *}
 
 section {* Antiquotations *}