diff -r 51c2635dd89c -r 2dcdea037385 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 02 23:12:09 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 02 23:12:23 2008 +0200
@@ -616,54 +616,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Definition by specification \label{sec:hol-specification}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
-    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
-  \end{matharray}
-
-  \begin{rail}
-  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
-  ;
-  decl: ((name ':')? term '(' 'overloaded' ')'?)
-  \end{rail}
-
-  \begin{descr}
-
-  \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
-  goal stating the existence of terms with the properties specified to
-  hold for the constants given in \isa{decls}.  After finishing the
-  proof, the theory will be augmented with definitions for the given
-  constants, as well as with theorems stating the properties for these
-  constants.
-
-  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
-  up a goal stating the existence of terms with the properties
-  specified to hold for the constants given in \isa{decls}.  After
-  finishing the proof, the theory will be augmented with axioms
-  expressing the properties given in the first place.
-
-  \item [\isa{decl}] declares a constant to be defined by the
-  specification given.  The definition for the constant \isa{c} is
-  bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
-  the declaration.  Overloaded constants should be declared as such.
-
-  \end{descr}
-
-  Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
-  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
-  user has explicitly proven it to be safe.  A practical issue must be
-  considered, though: After introducing two constants with the same
-  properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
-  that the two constants are, in fact, equal.  If this might be a
-  problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
 }
 \isamarkuptrue%
@@ -1140,6 +1092,54 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Definition by specification \label{sec:hol-specification}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
+    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
+  \end{matharray}
+
+  \begin{rail}
+  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
+  ;
+  decl: ((name ':')? term '(' 'overloaded' ')'?)
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
+  goal stating the existence of terms with the properties specified to
+  hold for the constants given in \isa{decls}.  After finishing the
+  proof, the theory will be augmented with definitions for the given
+  constants, as well as with theorems stating the properties for these
+  constants.
+
+  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
+  up a goal stating the existence of terms with the properties
+  specified to hold for the constants given in \isa{decls}.  After
+  finishing the proof, the theory will be augmented with axioms
+  expressing the properties given in the first place.
+
+  \item [\isa{decl}] declares a constant to be defined by the
+  specification given.  The definition for the constant \isa{c} is
+  bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
+  the declaration.  Overloaded constants should be declared as such.
+
+  \end{descr}
+
+  Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
+  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
+  user has explicitly proven it to be safe.  A practical issue must be
+  considered, though: After introducing two constants with the same
+  properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
+  that the two constants are, in fact, equal.  If this might be a
+  problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory