# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1221518625 -7200
# Node ID 007e09485351bb409341ee0aec0d01b6dca3c0bf
# Parent  e91f54791e14eb630d269e1d73b5bc8183cf4806
some tuning

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 *}
diff -r e91f54791e14 -r 007e09485351 CookBook/Intro.thy
--- a/CookBook/Intro.thy	Tue Sep 09 14:57:23 2008 +0200
+++ b/CookBook/Intro.thy	Tue Sep 16 00:43:45 2008 +0200
@@ -15,8 +15,8 @@
 
 text {* 
   This cookbook targets an audience who already knows how to use Isabelle
-  for writing theories and proofs. It is also assumed that the reader is 
-  familiar with the \emph{Standard ML} programming language, in which  
+  for writing theories and proofs. We also assume that readers are 
+  familiar with the Standard ML, the programming language in which  
   most of Isabelle is implemented. If you are unfamiliar with any of
   these two subjects, you should first work through the Isabelle/HOL
   tutorial \cite{isa-tutorial} and Paulson's book on Standard ML
@@ -28,18 +28,18 @@
 
 text {*
   
-  The following documents about ML-coding for Isabelle already exist (they are
-  included in the Isabelle distribution):
+  The following documentation about Isabelle programming already exist (they are
+  included in the distribution of Isabelle):
 
   \begin{description}
   \item[The Implementation Manual] describes Isabelle
   from a programmer's perspective, documenting both the underlying
-  concepts and the concrete interfaces. 
+  concepts and some of the interfaces. 
 
   \item[The Isabelle Reference Manual] is an older document that used
-  to be the main reference, when all reasoning happened on the ML
-  level. Many parts of it are outdated now, but some parts, mainly the
-  chapters on tactics, are still useful.
+  to be the main reference at a time when all proof scripts were written 
+  on the ML level. Many parts of this manual are outdated now, but some 
+  parts, mainly the chapters on tactics, are still useful.
   \end{description}
 
   Then of ourse there is:
diff -r e91f54791e14 -r 007e09485351 cookbook.pdf
Binary file cookbook.pdf has changed