diff -r ea22f2380871 -r 5f88c142676d src/Doc/Prog_Prove/Isar.thy
--- 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}