# HG changeset patch
# User skalberg
# Date 1061919184 -7200
# Node ID 67b4c4cdb270a43d9496bef34c4510ba92e28c41
# Parent  8c3fab5962193b6d61af75a7a7849e4bb379b607
New specification syntax added (the specification may be split over
several properties).

diff -r 8c3fab596219 -r 67b4c4cdb270 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Tue Aug 26 18:49:17 2003 +0200
+++ b/doc-src/IsarRef/logics.tex	Tue Aug 26 19:33:04 2003 +0200
@@ -541,18 +541,17 @@
 \end{matharray}
 
 \begin{rail}
-'specification' '(' (decl +) ')' thmdecl? prop
+'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 [$\isarkeyword{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 definitions for the given constants,
+  as well as with theorems stating the properties for these constants.
 \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.
@@ -728,7 +727,7 @@
   \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
-HOLCF provides a separate type for continuous functions $\alpha \rightarrow
+HOLCF provides a separate type for continuous functions $\alpha \to
 \beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
 syntax normally refers directly to the pure meta-level function type $\alpha
 \To \beta$, with application $f\,x$.