--- 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:
--- 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}
--- 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
*}
(*<*)
--- 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