src/Doc/Prog_Prove/Bool_nat_list.thy

 Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"},
 or @{term"Cons x (Cons y Nil)"}, etc.
 \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: *}
 
 fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "app Nil ys = ys" |

 \subsubsection{Structural Induction for Lists}
 
 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
 \item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}.
 \end{enumerate}