# HG changeset patch
# User wenzelm
# Date 1212589906 -7200
# Node ID f64166dd92f05c9b6f6e865e023be04426f3af79
# Parent  e104481d289d3459e94d3d695b6ee071ad619ba6
moved labels into actual sections;

diff -r e104481d289d -r f64166dd92f0 doc-src/Locales/Locales/Examples1.thy
--- 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
diff -r e104481d289d -r f64166dd92f0 doc-src/Locales/Locales/Examples3.thy
--- 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