# HG changeset patch
# User wenzelm
# Date 1284125995 -7200
# Node ID deab5d9c1ef1e911af73c5b1103c41dae17f4047
# Parent  878d86983dc1b17bc866045e56e15d8df15b30a7
updated generated file;

diff -r 878d86983dc1 -r deab5d9c1ef1 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Sep 10 15:38:54 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Sep 10 15:39:55 2010 +0200
@@ -1107,7 +1107,6 @@
   \begin{matharray}{rcl}
     \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
-    \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   \end{matharray}
 
   \begin{rail}
@@ -1117,18 +1116,6 @@
     ;
   \end{rail}
 
-  \begin{rail}
-    'constdefs' structs? (constdecl? constdef +)
-    ;
-
-    structs: '(' 'structure' (vars + 'and') ')'
-    ;
-    constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
-    ;
-    constdef: thmdecl? prop
-    ;
-  \end{rail}
-
   \begin{description}
 
   \item \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}} declares constant \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}.  The optional
@@ -1148,24 +1135,6 @@
   message would be issued for any definitional equation with a more
   special type than that of the corresponding constant declaration.
   
-  \item \hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}} combines constant declarations and
-  definitions, with type-inference taking care of the most general
-  typing of the given specification (the optional type constraint may
-  refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual).  The
-  resulting type declaration needs to agree with that of the
-  specification; overloading is \emph{not} supported here!
-  
-  The constant name may be omitted altogether, if neither type nor
-  syntax declarations are given.  The canonical name of the
-  definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
-  unless specified otherwise.  Also note that the given list of
-  specifications is processed in a strictly sequential manner, with
-  type-checking being performed independently.
-  
-  An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
-  admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'').  The latter concept is
-  particularly useful with locales (see also \secref{sec:locale}).
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%