# HG changeset patch
# User wenzelm
# Date 1212441111 -7200
# Node ID 4e7ecec1b685618db4e50a351cf5b5aaad5a2cc2
# Parent  c4eaa7140532fe730165827c030f22a94af8b1b7
moved (ax_)specification to end;

diff -r c4eaa7140532 -r 4e7ecec1b685 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jun 02 23:11:24 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jun 02 23:11:51 2008 +0200
@@ -614,55 +614,6 @@
 *}
 
 
-section {* Definition by specification \label{sec:hol-specification} *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\
-    @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\
-  \end{matharray}
-
-  \begin{rail}
-  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
-  ;
-  decl: ((name ':')? term '(' 'overloaded' ')'?)
-  \end{rail}
-
-  \begin{descr}
-
-  \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a
-  goal stating the existence of terms with the properties specified to
-  hold for the constants given in @{text 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 [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets
-  up a goal stating the existence of terms with the properties
-  specified to hold for the constants given in @{text decls}.  After
-  finishing the proof, the theory will be augmented with axioms
-  expressing the properties given in the first place.
-
-  \item [@{text decl}] declares a constant to be defined by the
-  specification given.  The definition for the constant @{text c} is
-  bound to the name @{text c_def} unless a theorem name is given in
-  the declaration.  Overloaded constants should be declared as such.
-
-  \end{descr}
-
-  Whether to use @{command (HOL) "specification"} or @{command (HOL)
-  "ax_specification"} is to some extent a matter of style.  @{command
-  (HOL) "specification"} introduces no new axioms, and so by
-  construction cannot introduce inconsistencies, whereas @{command
-  (HOL) "ax_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 @{command (HOL) "specification"}, one can prove
-  that the two constants are, in fact, equal.  If this might be a
-  problem, one should use @{command (HOL) "ax_specification"}.
-*}
-
-
 section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
 
 text {*
@@ -1139,4 +1090,53 @@
   \end{descr}
 *}
 
+
+section {* Definition by specification \label{sec:hol-specification} *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\
+    @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\
+  \end{matharray}
+
+  \begin{rail}
+  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
+  ;
+  decl: ((name ':')? term '(' 'overloaded' ')'?)
+  \end{rail}
+
+  \begin{descr}
+
+  \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a
+  goal stating the existence of terms with the properties specified to
+  hold for the constants given in @{text 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 [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets
+  up a goal stating the existence of terms with the properties
+  specified to hold for the constants given in @{text decls}.  After
+  finishing the proof, the theory will be augmented with axioms
+  expressing the properties given in the first place.
+
+  \item [@{text decl}] declares a constant to be defined by the
+  specification given.  The definition for the constant @{text c} is
+  bound to the name @{text c_def} unless a theorem name is given in
+  the declaration.  Overloaded constants should be declared as such.
+
+  \end{descr}
+
+  Whether to use @{command (HOL) "specification"} or @{command (HOL)
+  "ax_specification"} is to some extent a matter of style.  @{command
+  (HOL) "specification"} introduces no new axioms, and so by
+  construction cannot introduce inconsistencies, whereas @{command
+  (HOL) "ax_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 @{command (HOL) "specification"}, one can prove
+  that the two constants are, in fact, equal.  If this might be a
+  problem, one should use @{command (HOL) "ax_specification"}.
+*}
+
 end