1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Sep 08 10:45:55 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Sep 08 13:22:24 2010 +0200
     1.3 @@ -1069,7 +1069,6 @@
     1.4    \begin{matharray}{rcl}
     1.5      @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
     1.6      @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
     1.7 -    @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
     1.8    \end{matharray}
     1.9  
    1.10    \begin{rail}
    1.11 @@ -1079,18 +1078,6 @@
    1.12      ;
    1.13    \end{rail}
    1.14  
    1.15 -  \begin{rail}
    1.16 -    'constdefs' structs? (constdecl? constdef +)
    1.17 -    ;
    1.18 -
    1.19 -    structs: '(' 'structure' (vars + 'and') ')'
    1.20 -    ;
    1.21 -    constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
    1.22 -    ;
    1.23 -    constdef: thmdecl? prop
    1.24 -    ;
    1.25 -  \end{rail}
    1.26 -
    1.27    \begin{description}
    1.28  
    1.29    \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
    1.30 @@ -1111,25 +1098,6 @@
    1.31    message would be issued for any definitional equation with a more
    1.32    special type than that of the corresponding constant declaration.
    1.33    
    1.34 -  \item @{command "constdefs"} combines constant declarations and
    1.35 -  definitions, with type-inference taking care of the most general
    1.36 -  typing of the given specification (the optional type constraint may
    1.37 -  refer to type-inference dummies ``@{text _}'' as usual).  The
    1.38 -  resulting type declaration needs to agree with that of the
    1.39 -  specification; overloading is \emph{not} supported here!
    1.40 -  
    1.41 -  The constant name may be omitted altogether, if neither type nor
    1.42 -  syntax declarations are given.  The canonical name of the
    1.43 -  definitional axiom for constant @{text c} will be @{text c_def},
    1.44 -  unless specified otherwise.  Also note that the given list of
    1.45 -  specifications is processed in a strictly sequential manner, with
    1.46 -  type-checking being performed independently.
    1.47 -  
    1.48 -  An optional initial context of @{text "(structure)"} declarations
    1.49 -  admits use of indexed syntax, using the special symbol @{verbatim
    1.50 -  "\<index>"} (printed as ``@{text "\<index>"}'').  The latter concept is
    1.51 -  particularly useful with locales (see also \secref{sec:locale}).
    1.52 -
    1.53    \end{description}
    1.54  *}
    1.55