1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jun 02 23:11:24 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jun 02 23:11:51 2008 +0200
     1.3 @@ -614,55 +614,6 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -section {* Definition by specification \label{sec:hol-specification} *}
     1.8 -
     1.9 -text {*
    1.10 -  \begin{matharray}{rcl}
    1.11 -    @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\
    1.12 -    @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\
    1.13 -  \end{matharray}
    1.14 -
    1.15 -  \begin{rail}
    1.16 -  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
    1.17 -  ;
    1.18 -  decl: ((name ':')? term '(' 'overloaded' ')'?)
    1.19 -  \end{rail}
    1.20 -
    1.21 -  \begin{descr}
    1.22 -
    1.23 -  \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a
    1.24 -  goal stating the existence of terms with the properties specified to
    1.25 -  hold for the constants given in @{text decls}.  After finishing the
    1.26 -  proof, the theory will be augmented with definitions for the given
    1.27 -  constants, as well as with theorems stating the properties for these
    1.28 -  constants.
    1.29 -
    1.30 -  \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets
    1.31 -  up a goal stating the existence of terms with the properties
    1.32 -  specified to hold for the constants given in @{text decls}.  After
    1.33 -  finishing the proof, the theory will be augmented with axioms
    1.34 -  expressing the properties given in the first place.
    1.35 -
    1.36 -  \item [@{text decl}] declares a constant to be defined by the
    1.37 -  specification given.  The definition for the constant @{text c} is
    1.38 -  bound to the name @{text c_def} unless a theorem name is given in
    1.39 -  the declaration.  Overloaded constants should be declared as such.
    1.40 -
    1.41 -  \end{descr}
    1.42 -
    1.43 -  Whether to use @{command (HOL) "specification"} or @{command (HOL)
    1.44 -  "ax_specification"} is to some extent a matter of style.  @{command
    1.45 -  (HOL) "specification"} introduces no new axioms, and so by
    1.46 -  construction cannot introduce inconsistencies, whereas @{command
    1.47 -  (HOL) "ax_specification"} does introduce axioms, but only after the
    1.48 -  user has explicitly proven it to be safe.  A practical issue must be
    1.49 -  considered, though: After introducing two constants with the same
    1.50 -  properties using @{command (HOL) "specification"}, one can prove
    1.51 -  that the two constants are, in fact, equal.  If this might be a
    1.52 -  problem, one should use @{command (HOL) "ax_specification"}.
    1.53 -*}
    1.54 -
    1.55 -
    1.56  section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
    1.57  
    1.58  text {*
    1.59 @@ -1139,4 +1090,53 @@
    1.60    \end{descr}
    1.61  *}
    1.62  
    1.63 +
    1.64 +section {* Definition by specification \label{sec:hol-specification} *}
    1.65 +
    1.66 +text {*
    1.67 +  \begin{matharray}{rcl}
    1.68 +    @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\
    1.69 +    @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\
    1.70 +  \end{matharray}
    1.71 +
    1.72 +  \begin{rail}
    1.73 +  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
    1.74 +  ;
    1.75 +  decl: ((name ':')? term '(' 'overloaded' ')'?)
    1.76 +  \end{rail}
    1.77 +
    1.78 +  \begin{descr}
    1.79 +
    1.80 +  \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a
    1.81 +  goal stating the existence of terms with the properties specified to
    1.82 +  hold for the constants given in @{text decls}.  After finishing the
    1.83 +  proof, the theory will be augmented with definitions for the given
    1.84 +  constants, as well as with theorems stating the properties for these
    1.85 +  constants.
    1.86 +
    1.87 +  \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets
    1.88 +  up a goal stating the existence of terms with the properties
    1.89 +  specified to hold for the constants given in @{text decls}.  After
    1.90 +  finishing the proof, the theory will be augmented with axioms
    1.91 +  expressing the properties given in the first place.
    1.92 +
    1.93 +  \item [@{text decl}] declares a constant to be defined by the
    1.94 +  specification given.  The definition for the constant @{text c} is
    1.95 +  bound to the name @{text c_def} unless a theorem name is given in
    1.96 +  the declaration.  Overloaded constants should be declared as such.
    1.97 +
    1.98 +  \end{descr}
    1.99 +
   1.100 +  Whether to use @{command (HOL) "specification"} or @{command (HOL)
   1.101 +  "ax_specification"} is to some extent a matter of style.  @{command
   1.102 +  (HOL) "specification"} introduces no new axioms, and so by
   1.103 +  construction cannot introduce inconsistencies, whereas @{command
   1.104 +  (HOL) "ax_specification"} does introduce axioms, but only after the
   1.105 +  user has explicitly proven it to be safe.  A practical issue must be
   1.106 +  considered, though: After introducing two constants with the same
   1.107 +  properties using @{command (HOL) "specification"}, one can prove
   1.108 +  that the two constants are, in fact, equal.  If this might be a
   1.109 +  problem, one should use @{command (HOL) "ax_specification"}.
   1.110 +*}
   1.111 +
   1.112  end