diff -r e8f11280c762 -r 76cdc8f562fc CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Mar 03 13:00:55 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Mar 04 13:15:29 2009 +0000
@@ -18,6 +18,9 @@
   \ldots
   \end{tabular}
   \end{center}
+
+  We also generally assume you are working with HOL. The given examples might
+  need to be adapted slightly if you work in a different logic.
 *}
 
 section {* Including ML-Code *}
@@ -468,7 +471,7 @@
   \end{readmore}
 
   Sometimes the internal representation of terms can be surprisingly different
-  from what you see at the user level, because the layers of
+  from what you see at the user-level, because the layers of
   parsing/type-checking/pretty printing can be quite elaborate. 
 
   \begin{exercise}
@@ -1085,7 +1088,7 @@
   for adding and deleting theorems) and an internal ML interface to retrieve and 
   modify the theorems.
 
-  Furthermore, the facts are made available on the user level under the dynamic 
+  Furthermore, the facts are made available on the user-level under the dynamic 
   fact name @{text foo}. For example you can declare three lemmas to be of the kind
   @{text foo} by:
 *}