# HG changeset patch
# User skalberg
# Date 1082225063 -7200
# Node ID 8876ad83b1fbc103de35c69f8075ae36c7175ba9
# Parent  068bb99f3ebd18e386df0d61138f27f7d663dbcf
Added documentation for ax_specification, as well as a small comparison of
ax_specification and specification.

diff -r 068bb99f3ebd -r 8876ad83b1fb doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Sat Apr 17 17:08:53 2004 +0200
+++ b/doc-src/IsarRef/logics.tex	Sat Apr 17 20:04:23 2004 +0200
@@ -538,10 +538,11 @@
 \indexisarcmdof{HOL}{specification}
 \begin{matharray}{rcl}
   \isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\
+  \isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\
 \end{matharray}
 
 \begin{rail}
-'specification' '(' (decl +) ')' (thmdecl? prop +)
+('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
 ;
 decl: ((name ':')? term '(overloaded)'?)
 \end{rail}
@@ -552,12 +553,26 @@
   constants given in $\mathit{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 [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating
+  the existence of terms with the properties specified to hold for the
+  constants given in $\mathit{decls}$.  After finishing the proof, the
+  theory will be augmented with axioms expressing the properties given
+  in the first place.
 \item[$decl$] declares a constant to be defined by the specification
   given.  The definition for the constant $c$ is bound to the name
   $c$\_def unless a theorem name is given in the declaration.
   Overloaded constants should be declared as such.
 \end{descr}
 
+Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$
+is to some extent a matter of style.  $\isarkeyword{specification}$ introduces no new axioms,
+and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{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 $\isarkeyword{specification}$, one can prove
+that the two constants are, in fact, equal.  If this might be a problem,
+one should use $\isarkeyword{ax_specification}$.
+
 \subsection{(Co)Inductive sets}\label{sec:hol-inductive}
 
 \indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}