--- 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