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

 level of classes and the results will be applicable to all types in a class,
 just as in axiomatic mathematics. These ideas are demonstrated by means of
 our above ordering relations.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Partial orders%
+\isamarkupsubsubsection{Partial Orders%
 }
 %
 \begin{isamarkuptext}%
 A \emph{partial order} is a subclass of \isa{ordrel}
 where certain axioms need to hold:%

 \noindent
 The first three axioms are the familiar ones, and the final one
 requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected.
 Note that behind the scenes, Isabelle has restricted the axioms to class
 \isa{parord}. For example, this is what \isa{refl} really looks like:
-\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
+\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
 
 We have not made \isa{less{\isacharunderscore}le} a global definition because it would
 fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}}.
 There are however situations where it is the other way around, which such a
 definition would complicate. The slight drawback of the above class is that

 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{by}\ simp%
 \begin{isamarkuptext}%
 \noindent
-The effect is not stunning but demonstrates the principle.  It also shows
+The effect is not stunning, but it demonstrates the principle.  It also shows
 that tools like the simplifier can deal with generic rules as well. Moreover,
 it should be clear that the main advantage of the axiomatic method is that
 theorems can be proved in the abstract and one does not need to repeat the
 proof for each instance.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Linear orders%
+\isamarkupsubsubsection{Linear Orders%
 }
 %
 \begin{isamarkuptext}%
 If any two elements of a partial order are comparable it is a
 \emph{linear} or \emph{total} order:%

 common case. It is also possible to prove additional subclass relationships
 later on, i.e.\ subclassing by proof. This is the topic of the following
 paragraph.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Strict orders%
+\isamarkupsubsubsection{Strict Orders%
 }
 %
 \begin{isamarkuptext}%
 An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
 \isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \emph{strict} order:%

 \begin{isamarkuptext}%
 The subclass relation must always be acyclic. Therefore Isabelle will
 complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Multiple inheritance and sorts%
+\isamarkupsubsubsection{Multiple Inheritance and Sorts%
 }
 %
 \begin{isamarkuptext}%
 A class may inherit from more than one direct superclass. This is called
 multiple inheritance and is certainly permitted. For example we could define

 \isa{linord} & & & & \isa{wford} \\
 & \backslash & & / \\
 & & \isa{wellord}
 \end{array}
 \]
-\caption{Subclass diagramm}
+\caption{Subclass Diagram}
 \label{fig:subclass}
 \end{figure}
 
 Since class \isa{wellord} does not introduce any new axioms, it can simply
 be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on