--- a/src/Doc/Prog_Prove/Basics.thy Thu Oct 02 17:51:04 2014 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy Fri Oct 03 11:48:27 2014 +0200
@@ -27,7 +27,7 @@
\item[function types,]
denoted by @{text"\<Rightarrow>"}.
\item[type variables,]
- denoted by @{typ 'a}, @{typ 'b}, etc., just like in ML\@.
+ denoted by @{typ 'a}, @{typ 'b}, etc., like in ML\@.
\end{description}
Note that @{typ"'a \<Rightarrow> 'b list"} means @{typ[source]"'a \<Rightarrow> ('b list)"},
not @{typ"('a \<Rightarrow> 'b) list"}: postfix type constructors have precedence
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Thu Oct 02 17:51:04 2014 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Fri Oct 03 11:48:27 2014 +0200
@@ -94,7 +94,7 @@
\begin{warn}
Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard
arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"},
- @{text"<"} etc) are overloaded: they are available
+ @{text"<"}, etc.) are overloaded: they are available
not just for natural numbers but for other types as well.
For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
@@ -150,7 +150,7 @@
\subsection{Type \indexed{@{text list}}{list}}
-Although lists are already predefined, we define our own copy just for
+Although lists are already predefined, we define our own copy for
demonstration purposes:
*}
(*<*)
@@ -211,7 +211,7 @@
\begin{figure}[htbp]
\begin{alltt}
\input{MyList.thy}\end{alltt}
-\caption{A Theory of Lists}
+\caption{A theory of lists}
\label{fig:MyList}
\index{comment}
\end{figure}
--- a/src/Doc/Prog_Prove/Isar.thy Thu Oct 02 17:51:04 2014 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Fri Oct 03 11:48:27 2014 +0200
@@ -73,7 +73,7 @@
Propositions are optionally named formulas. These names can be referred to in
later \isacom{from} clauses. In the simplest case, a fact is such a name.
But facts can also be composed with @{text OF} and @{text of} as shown in
-\S\ref{sec:forward-proof}---hence the \dots\ in the above grammar. Note
+\autoref{sec:forward-proof}---hence the \dots\ in the above grammar. Note
that assumptions, intermediate \isacom{have} statements and global lemmas all
have the same status and are thus collectively referred to as
\conceptidx{facts}{fact}.
@@ -217,7 +217,7 @@
Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer
-to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc.\
+to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc.,
thus obviating the need to name them individually.
\section{Proof Patterns}
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Thu Oct 02 17:51:04 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Fri Oct 03 11:48:27 2014 +0200
@@ -8,11 +8,11 @@
\section{Type and Function Definitions}
Type synonyms are abbreviations for existing types, for example
-*}
+\index{string@@{text string}}*}
type_synonym string = "char list"
-text{*\index{string@@{text string}}
+text{*
Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
\subsection{Datatypes}
@@ -118,7 +118,7 @@
"sq' n \<equiv> n * n"
text{* The key difference is that @{const sq'} is only syntactic sugar:
-after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}, and
+after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}};
before printing, every occurrence of @{term"u*u"} is replaced by
\mbox{@{term"sq' u"}}. Internally, @{const sq'} does not exist.
This is the
@@ -411,7 +411,7 @@
Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and
@{prop"xs @ [] = xs"}, should be declared as simplification
rules. Equations that may be counterproductive as simplification rules
-should only be used in specific proof steps (see \S\ref{sec:simp} below).
+should only be used in specific proof steps (see \autoref{sec:simp} below).
Distributivity laws, for example, alter the structure of terms
and can produce an exponential blow-up.