# HG changeset patch
# User nipkow
# Date 1384764350 -3600
# Node ID 663a927fdc88e9950f3e58dbd127d46e4a1bbda7
# Parent  d0457655740046f6eda789014e587767cd7c83c3
comments by Sean Seefried

diff -r d04576557400 -r 663a927fdc88 src/Doc/ProgProve/Basics.thy
--- a/src/Doc/ProgProve/Basics.thy	Sun Nov 17 22:50:09 2013 +0100
+++ b/src/Doc/ProgProve/Basics.thy	Mon Nov 18 09:45:50 2013 +0100
@@ -22,8 +22,8 @@
 \item[type constructors,]
  in particular @{text list}, the type of
 lists, and @{text set}, the type of sets. Type constructors are written
-postfix, e.g.\ @{typ "nat list"} is the type of lists whose elements are
-natural numbers.
+postfix, i.e., after their arguments. For example,
+@{typ "nat list"} is the type of lists whose elements are natural numbers.
 \item[function types,]
 denoted by @{text"\<Rightarrow>"}.
 \item[type variables,]
@@ -41,8 +41,8 @@
 \begin{warn}
 There are many predefined infix symbols like @{text "+"} and @{text"\<le>"}.
 The name of the corresponding binary function is @{term"op +"},
-not just @{text"+"}. That is, @{term"x + y"} is syntactic sugar for
-\noquotes{@{term[source]"op + x y"}}.
+not just @{text"+"}. That is, @{term"x + y"} is nice surface syntax
+(``syntactic sugar'') for \noquotes{@{term[source]"op + x y"}}.
 \end{warn}
 
 HOL also supports some basic constructs from functional programming:
diff -r d04576557400 -r 663a927fdc88 src/Doc/ProgProve/Bool_nat_list.thy
--- a/src/Doc/ProgProve/Bool_nat_list.thy	Sun Nov 17 22:50:09 2013 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy	Mon Nov 18 09:45:50 2013 +0100
@@ -372,10 +372,10 @@
 ys zs)"}. It appears almost mysterious because we suddenly complicate the
 term by appending @{text Nil} on the left. What is really going on is this:
 when proving some equality \mbox{@{prop"s = t"}}, both @{text s} and @{text t} are
-simplified to some common term @{text u}.  This heuristic for equality proofs
+simplified until they ``meet in the middle''. This heuristic for equality proofs
 works well for a functional programming context like ours. In the base case
-@{text s} is @{term"app (app Nil ys) zs"}, @{text t} is @{term"app Nil (app
-ys zs)"}, and @{text u} is @{term"app ys zs"}.
+both @{term"app (app Nil ys) zs"} and @{term"app Nil (app
+ys zs)"} are simplified to @{term"app ys zs"}, the term in the middle.
 
 \subsection{Predefined Lists}
 \label{sec:predeflists}
@@ -429,7 +429,7 @@
 
 \begin{exercise}
 Start from the definition of @{const add} given above.
-Prove that @{const add} it is associative and commutative.
+Prove that @{const add} is associative and commutative.
 Define a recursive function @{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"}
 and prove @{prop"double m = add m m"}.
 \end{exercise}
diff -r d04576557400 -r 663a927fdc88 src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Sun Nov 17 22:50:09 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Mon Nov 18 09:45:50 2013 +0100
@@ -528,7 +528,7 @@
 \exercise\label{exe:tree0}
 Define a datatype @{text tree0} of binary tree skeletons which do not store
 any information, neither in the inner nodes nor in the leaves.
-Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the total number
+Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of
 all nodes (inner nodes and leaves) in such a tree.
 Consider the following recursive function:
 *}
@@ -571,7 +571,7 @@
 that transforms an expression into a polynomial. This may require auxiliary
 functions. Prove that @{text coeffs} preserves the value of the expression:
 \mbox{@{prop"evalp (coeffs e) x = eval e x"}.}
-Hint: consider the hint in \autoref{exe:tree0}.
+Hint: consider the hint in Exercise~\ref{exe:tree0}.
 \endexercise
 *}
 (*<*)
diff -r d04576557400 -r 663a927fdc88 src/Doc/ProgProve/document/intro-isabelle.tex
--- a/src/Doc/ProgProve/document/intro-isabelle.tex	Sun Nov 17 22:50:09 2013 +0100
+++ b/src/Doc/ProgProve/document/intro-isabelle.tex	Mon Nov 18 09:45:50 2013 +0100
@@ -88,7 +88,6 @@
 
 \ifsem\else
 \paragraph{Acknowledgements}
-I wish to thank the following people for their comments
-on this document:
-Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.
+I wish to thank the following people for their comments on this document:
+Florian Haftmann, Ren\'{e} Thiemann, Sean Seefried and Christian Sternagel.
 \fi
\ No newline at end of file