diff -r 616f58da9db0 -r f9f3ecc949c5 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Jul 21 13:15:21 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 21 13:22:17 2009 +0200
@@ -913,27 +913,6 @@
   "writeln (Syntax.string_of_term @{context}
    (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
   "True = False"}
-
-  \begin{readmore}
-  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
-  @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
-  and types easier.\end{readmore}
-
-  Have a look at these files and try to solve the following two exercises:
-
-  \begin{exercise}\label{fun:revsum}
-  Write a function @{text "rev_sum : term -> term"} that takes a
-  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
-  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
-  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
-  associates to the left. Try your function on some examples. 
-  \end{exercise}
-
-  \begin{exercise}\label{fun:makesum}
-  Write a function which takes two terms representing natural numbers
-  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
-  number representing their sum.
-  \end{exercise}
 *}
 
 section {* Constants *}
@@ -1022,7 +1001,28 @@
   | is_nil_or_all _ = false *}
 
 text {*
-  The antiquotation for properly referencing type constants is  is @{text "@{type_name \<dots>}"}.
+  \begin{readmore}
+  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
+  @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
+  and types easier.\end{readmore}
+
+  Have a look at these files and try to solve the following two exercises:
+
+  \begin{exercise}\label{fun:revsum}
+  Write a function @{text "rev_sum : term -> term"} that takes a
+  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
+  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
+  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
+  associates to the left. Try your function on some examples. 
+  \end{exercise}
+
+  \begin{exercise}\label{fun:makesum}
+  Write a function which takes two terms representing natural numbers
+  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
+  number representing their sum.
+  \end{exercise}
+
+  The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
   For example
 
   @{ML_response [display,gray]