# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1248775893 -7200
# Node ID 0a567f923b42b35f88999ad063870867a06bb1e7
# Parent  41a802bbb7df8a292dd4a766cd6098f643d1c704
slightly changed exercises about rev_sum

diff -r 41a802bbb7df -r 0a567f923b42 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Jul 28 08:53:05 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 28 12:11:33 2009 +0200
@@ -1218,9 +1218,11 @@
   the file @{ML_file "Pure/thm.ML"}.
   \end{readmore}
 
-  \begin{exercise}\label{fun:revsum typed}
+  \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
-  result that type-checks.
+  result that type-checks. See what happens to the  solutions of this 
+  exercise given in \ref{ch:solutions} when they receive an ill-typed term
+  as input.
   \end{exercise}
 
   Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 
diff -r 41a802bbb7df -r 0a567f923b42 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Tue Jul 28 08:53:05 2009 +0200
+++ b/ProgTutorial/Intro.thy	Tue Jul 28 12:11:33 2009 +0200
@@ -211,10 +211,10 @@
   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
 
   \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 
-  chapter and also contributed the material on @{text NamedThmsFun}.
+  chapter and also contributed the material on @{ML_functor Named_Thms}.
 
   \item {\bf Christian Sternagel} proofread the tutorial and made 
-  many comments on the text. 
+  many improvemets to the text. 
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining
diff -r 41a802bbb7df -r 0a567f923b42 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Tue Jul 28 08:53:05 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Tue Jul 28 12:11:33 2009 +0200
@@ -6,10 +6,13 @@
 
 text {* \solution{fun:revsum} *}
 
-ML{*fun rev_sum((p as Const(@{const_name plus},_)) $ t $ u) = p $ u $ rev_sum t
+ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = 
+      p $ u $ rev_sum t
   | rev_sum t = t *}
 
-text {* \solution{fun:revsum typed} *}
+text {* 
+  An alternative solution using the function @{ML [index] mk_binop in HOLogic} is:
+ *}
 
 ML{*fun rev_sum t =
 let
@@ -19,8 +22,6 @@
    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 end *}
 
-
-
 text {* \solution{fun:makesum} *}
 
 ML{*fun make_sum t1 t2 =
diff -r 41a802bbb7df -r 0a567f923b42 ProgTutorial/document/root.tex
--- a/ProgTutorial/document/root.tex	Tue Jul 28 08:53:05 2009 +0200
+++ b/ProgTutorial/document/root.tex	Tue Jul 28 12:11:33 2009 +0200
@@ -152,7 +152,8 @@
         Jasmin & Blanchette\\
         Sascha & Böhme\\
         Jeremy & Dawson\\
-        Alexander & Krauss\\ 
+        Alexander & Krauss\\
+        Christian & Sternagel\\ 
         \end{tabular}}
 
 \maketitle
diff -r 41a802bbb7df -r 0a567f923b42 progtutorial.pdf
Binary file progtutorial.pdf has changed