diff -r f56fc3305a08 -r 615780a701b6 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Thu Nov 17 12:20:19 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Thu Nov 17 16:33:49 2011 +0000
@@ -76,8 +76,8 @@
   \end{isabelle}
   \end{quote}
 
-  However, both commands will only play minor roles in this tutorial (we will
-  always arrange that the ML-code is defined outside proofs).
+  However, both commands will only play minor roles in this tutorial (we most of
+  the time make sure that the ML-code is defined outside proofs).
 
   
 
@@ -211,11 +211,14 @@
 
   where now even @{term Pair} is written with its type (@{term Pair} is the
   term-constructor for products). Other configuration values that influence
-  printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind
-  show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}.
-*}
+  printing of terms include 
 
-text {*
+  \begin{itemize}
+  \item @{ML_ind show_brackets in Syntax} 
+  \item @{ML_ind show_sorts in Syntax}
+  \item @{ML_ind eta_contract in Syntax}
+  \end{itemize}
+
   A @{ML_type cterm} can be printed with the following function.
 *}
 
@@ -689,8 +692,8 @@
   pwriteln (pretty_term ctxt' one_trm);
   pwriteln (pretty_thm ctxt' one_thm)
 end"
-  "one
-one \<equiv> 1"}
+  "One
+One \<equiv> 1"}
   Recall that @{ML "|>"} is the reverse function application. Recall also that
   the related reverse function composition is @{ML "#>"}. In fact all the
   combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
@@ -701,8 +704,8 @@
 *}
 
 ML{*val double =
-            (fn x => (x, x))
-        #-> (fn x => fn y => x + y)*}
+   (fn x => (x, x)) #-> 
+   (fn x => fn y => x + y)*}
 
 
 text {*