# HG changeset patch
# User skalberg
# Date 1058777896 -7200
# Node ID fb9c392644a15e3ca05a5941d1b4b825785cb167
# Parent  05416ba8eef24aa7b2a7c14035821ffb76219ac1
Added the specification command.

diff -r 05416ba8eef2 -r fb9c392644a1 NEWS
--- a/NEWS	Mon Jul 21 08:53:56 2003 +0200
+++ b/NEWS	Mon Jul 21 10:58:16 2003 +0200
@@ -110,6 +110,9 @@
 
 *** HOL ***
 
+* 'specification' command added, allowing for definition by
+specification.
+
 * arith(_tac)
 
  - Produces a counter example if it cannot prove a goal.
diff -r 05416ba8eef2 -r fb9c392644a1 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Mon Jul 21 08:53:56 2003 +0200
+++ b/doc-src/IsarRef/logics.tex	Mon Jul 21 10:58:16 2003 +0200
@@ -533,6 +533,31 @@
   ;
 \end{rail}
 
+\subsection{Definition by specification}\label{sec:hol-specification}
+
+\indexisarcmdof{HOL}{specification}
+\begin{matharray}{rcl}
+  \isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\
+\end{matharray}
+
+\begin{rail}
+'specification' '(' (decl +) ')' thmdecl? prop
+;
+decl: ((name ':')? term '(overloaded)'?)
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{specification}~decls~\phi$] sets up a
+  goal stating the existence of terms with the property specified to
+  hold for the constants given in $\mathit{decls}$.  After finishing
+  the proof, the theory will be augmented with definitions for the
+  given constants, and a theorem stating the property for these
+  constants is returned.
+\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}
 
 \subsection{(Co)Inductive sets}\label{sec:hol-inductive}