# HG changeset patch
# User nipkow
# Date 1412329707 -7200
# Node ID b70e93c05efee50d738ecba9182c441e4e3b1dd5
# Parent  a4d1f8041af05243bb8ec816829ee3296c46232a
tuned

diff -r a4d1f8041af0 -r b70e93c05efe src/Doc/Prog_Prove/Basics.thy
--- 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
diff -r a4d1f8041af0 -r b70e93c05efe src/Doc/Prog_Prove/Bool_nat_list.thy
--- 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}
diff -r a4d1f8041af0 -r b70e93c05efe src/Doc/Prog_Prove/Isar.thy
--- 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}
diff -r a4d1f8041af0 -r b70e93c05efe src/Doc/Prog_Prove/Types_and_funs.thy
--- 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.