--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Tue Sep 30 19:37:34 2014 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Tue Sep 30 22:43:20 2014 +0200
@@ -169,7 +169,7 @@
\item \isacom{datatype} requires no quotation marks on the
left-hand side, but on the right-hand side each of the argument
types of a constructor needs to be enclosed in quotation marks, unless
-it is just an identifier (e.g.\ @{typ nat} or @{typ 'a}).
+it is just an identifier (e.g., @{typ nat} or @{typ 'a}).
\end{itemize}
We also define two standard functions, append and reverse: *}
@@ -221,7 +221,7 @@
Just as for natural numbers, there is a proof principle of induction for
lists. Induction over a list is essentially induction over the length of
the list, although the length remains implicit. To prove that some property
-@{text P} holds for all lists @{text xs}, i.e.\ \mbox{@{prop"P(xs)"}},
+@{text P} holds for all lists @{text xs}, i.e., \mbox{@{prop"P(xs)"}},
you need to prove
\begin{enumerate}
\item the base case @{prop"P(Nil)"} and
--- a/src/Doc/Prog_Prove/Isar.thy Tue Sep 30 19:37:34 2014 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Tue Sep 30 22:43:20 2014 +0200
@@ -59,7 +59,7 @@
method which must finish off the statement being proved, for example @{text
auto}, or it can be a \isacom{proof}--\isacom{qed} block of multiple
steps. Such a block can optionally begin with a proof method that indicates
-how to start off the proof, e.g.\ \mbox{@{text"(induction xs)"}}.
+how to start off the proof, e.g., \mbox{@{text"(induction xs)"}}.
A step either assumes a proposition or states a proposition
together with its proof. The optional \isacom{from} clause
@@ -721,7 +721,7 @@
text{*
The unknown @{text"?case"}\index{case?@@{text"?case"}|(} is set in each case to the required
-claim, i.e.\ @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof,
+claim, i.e., @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof,
without requiring the user to define a @{text "?P"}. The general
pattern for induction over @{typ nat} is shown on the left-hand side:
*}text_raw{*
@@ -935,7 +935,7 @@
induction rule. For rule inductions these are the hypotheses of rule
@{text name}, for structural inductions these are empty.
\item[@{text name.prems}]\index{prems@@{text".prems"}} contains the (suitably instantiated) premises
-of the statement being proved, i.e. the @{text A\<^sub>i} when
+of the statement being proved, i.e., the @{text A\<^sub>i} when
proving @{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}.
\end{description}
\begin{warn}
@@ -947,7 +947,7 @@
More complicated inductive proofs than the ones we have seen so far
often need to refer to specific assumptions---just @{text name} or even
@{text name.prems} and @{text name.IH} can be too unspecific.
-This is where the indexing of fact lists comes in handy, e.g.\
+This is where the indexing of fact lists comes in handy, e.g.,
@{text"name.IH(2)"} or @{text"name.prems(1-2)"}.
\subsection{Rule Inversion}
--- a/src/Doc/Prog_Prove/Logic.thy Tue Sep 30 19:37:34 2014 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Tue Sep 30 22:43:20 2014 +0200
@@ -197,7 +197,7 @@
A proof method that is still incomplete but tries harder than @{text auto} is
\indexed{@{text fastforce}}{fastforce}. It either succeeds or fails, it acts on the first
-subgoal only, and it can be modified just like @{text auto}, e.g.\
+subgoal only, and it can be modified just like @{text auto}, e.g.,
with @{text "simp add"}. Here is a typical example of what @{text fastforce}
can do:
*}
@@ -284,7 +284,7 @@
connectives @{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"}, @{text"\<longrightarrow>"},
@{text"\<longleftrightarrow>"}. Strictly speaking, this is known as \concept{linear arithmetic}
because it does not involve multiplication, although multiplication with
-numbers, e.g.\ @{text"2*n"}, is allowed. Such formulas can be proved by
+numbers, e.g., @{text"2*n"}, is allowed. Such formulas can be proved by
\indexed{@{text arith}}{arith}:
*}
@@ -399,7 +399,7 @@
{\mbox{@{text"?P = ?Q"}}}
\]
These rules are part of the logical system of \concept{natural deduction}
-(e.g.\ \cite{HuthRyan}). Although we intentionally de-emphasize the basic rules
+(e.g., \cite{HuthRyan}). Although we intentionally de-emphasize the basic rules
of logic in favour of automatic proof methods that allow you to take bigger
steps, these rules are helpful in locating where and why automation fails.
When applied backwards, these rules decompose the goal:
@@ -471,7 +471,7 @@
@{text dest} which instructs the proof method to use certain rules in a
forward fashion. If @{text r} is of the form \mbox{@{text "A \<Longrightarrow> B"}}, the modifier
\mbox{@{text"dest: r"}}\index{dest@@{text"dest:"}}
-allows proof search to reason forward with @{text r}, i.e.\
+allows proof search to reason forward with @{text r}, i.e.,
to replace an assumption @{text A'}, where @{text A'} unifies with @{text A},
with the correspondingly instantiated @{text B}. For example, @{thm[source,show_question_marks] Suc_leD} is the theorem \mbox{@{thm Suc_leD}}, which works well for forward reasoning:
*}
@@ -526,7 +526,7 @@
text{* To get used to inductive definitions, we will first prove a few
properties of @{const ev} informally before we descend to the Isabelle level.
-How do we prove that some number is even, e.g.\ @{prop "ev 4"}? Simply by combining the defining rules for @{const ev}:
+How do we prove that some number is even, e.g., @{prop "ev 4"}? Simply by combining the defining rules for @{const ev}:
\begin{quote}
@{text "ev 0 \<Longrightarrow> ev (0 + 2) \<Longrightarrow> ev((0 + 2) + 2) = ev 4"}
\end{quote}
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Tue Sep 30 19:37:34 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Tue Sep 30 22:43:20 2014 +0200
@@ -145,7 +145,7 @@
recursive calls on the right-hand side must be strictly smaller than the
arguments on the left-hand side. In the simplest case, this means that one
fixed argument position decreases in size with each recursive call. The size
-is measured as the number of constructors (excluding 0-ary ones, e.g.\ @{text
+is measured as the number of constructors (excluding 0-ary ones, e.g., @{text
Nil}). Lexicographic combinations are also recognized. In more complicated
situations, the user may have to prove termination by hand. For details
see~\cite{Krauss}.
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Sep 30 19:37:34 2014 +0200
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Sep 30 22:43:20 2014 +0200
@@ -64,7 +64,7 @@
\begin{center}
\includegraphics[width=\textwidth]{jedit.png}
\end{center}
-The upper part of the window shows the input typed by the user, i.e.\ the
+The upper part of the window shows the input typed by the user, i.e., the
gradually growing Isabelle text of definitions, theorems, proofs, etc. The
interface processes the user input automatically while it is typed, just like
modern Java IDEs. Isabelle's response to the user input is shown in the