--- a/doc-src/Locales/Locales/document/Examples1.tex Wed Jun 04 16:32:14 2008 +0200
+++ b/doc-src/Locales/Locales/document/Examples1.tex Wed Jun 04 16:32:24 2008 +0200
@@ -51,14 +51,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{First Version: Replacement of Parameters Only%
+\isamarkupsubsection{First Version: Replacement of Parameters Only \label{sec:po-first}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\label{sec:po-first}
-
- In the most basic form, interpretation just replaces the locale
+In the most basic form, interpretation just replaces the locale
parameters by terms. The following command interprets the locale
\isa{partial{\isacharunderscore}order} in the global context of the theory. The
parameter \isa{le} is replaced by \isa{op\ {\isasymle}}.%
--- a/doc-src/Locales/Locales/document/Examples3.tex Wed Jun 04 16:32:14 2008 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex Wed Jun 04 16:32:24 2008 +0200
@@ -444,14 +444,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Locale Expressions%
+\isamarkupsection{Locale Expressions \label{sec:expressions}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\label{sec:expressions}
-
- A map \isa{{\isasymphi}} between partial orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}
+A map \isa{{\isasymphi}} between partial orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}
is called order preserving if \isa{x\ {\isasymsqsubseteq}\ y} implies \isa{{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y}. This situation is more complex than those encountered so
far: it involves two partial orders, and it is desirable to use the
existing locale for both.