--- a/doc-src/Locales/Locales/Examples1.thy Wed Jun 04 16:31:16 2008 +0200
+++ b/doc-src/Locales/Locales/Examples1.thy Wed Jun 04 16:31:46 2008 +0200
@@ -38,11 +38,9 @@
*}
-subsection {* First Version: Replacement of Parameters Only *}
+subsection {* First Version: Replacement of Parameters Only \label{sec:po-first} *}
text {*
-\label{sec:po-first}
-
In the most basic form, interpretation just replaces the locale
parameters by terms. The following command interprets the locale
@{text partial_order} in the global context of the theory. The
--- a/doc-src/Locales/Locales/Examples3.thy Wed Jun 04 16:31:16 2008 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Wed Jun 04 16:31:46 2008 +0200
@@ -241,11 +241,9 @@
*}
-section {* Locale Expressions *}
+section {* Locale Expressions \label{sec:expressions} *}
text {*
-\label{sec:expressions}
-
A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>}
is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq>
\<phi> y"}. This situation is more complex than those encountered so