doc-src/TutorialI/Types/document/Typedef.tex

 need for a more advanced type. If you cannot avoid that type, and you are
 quite certain that it is not definable by any of the standard means,
 then read on.
 \begin{warn}
   Types in HOL must be non-empty; otherwise the quantifier rules would be
-  unsound, because $\exists x. x=x$ is a theorem.
+  unsound, because $\exists x.\ x=x$ is a theorem.
 \end{warn}%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Declaring new types%
 }

 declaration}:%
 \end{isamarkuptext}%
 \isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type%
 \begin{isamarkuptext}%
 \noindent\indexbold{*typedecl}%
-This does not define the type at all but merely introduces its name, \isa{my{\isacharunderscore}new{\isacharunderscore}type}. Thus we know nothing about this type, except that it is
+This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
+name. Thus we know nothing about this type, except that it is
 non-empty. Such declarations without definitions are
 useful only if that type can be viewed as a parameter of a theory and we do
 not intend to impose any restrictions on it. A typical example is given in
 \S\ref{sec:VMC}, where we define transition relations over an arbitrary type
 of states without any internal structure.

 If you are looking for a quick and dirty way of introducing a new type
 together with its properties: declare the type and state its properties as
 axioms. Example:%
 \end{isamarkuptext}%
 \isacommand{axioms}\isanewline
-just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}{\isacharbang}\ x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ True{\isachardoublequote}%
+just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 However, we strongly discourage this approach, except at explorative stages
 of your development. It is extremely easy to write down contradictory sets of
 axioms, in which case you will be able to prove everything but it will mean