doc-src/IsarRef/Thy/document/Spec.tex
changeset 36454 f2b5bcc61a8c
parent 36178 0e5c133b48b6
child 37115 9b27c3dccb01
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Apr 28 12:18:49 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Apr 28 12:21:55 2010 +0200
     1.3 @@ -937,7 +937,7 @@
     1.4  \begin{matharray}{rcll}
     1.5      \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.6      \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
     1.7 -    \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.8 +    \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     1.9      \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    1.10    \end{matharray}
    1.11  
    1.12 @@ -946,7 +946,7 @@
    1.13      ;
    1.14      'classrel' (nameref ('<' | subseteq) nameref + 'and')
    1.15      ;
    1.16 -    'defaultsort' sort
    1.17 +    'default\_sort' sort
    1.18      ;
    1.19    \end{rail}
    1.20  
    1.21 @@ -964,7 +964,7 @@
    1.22    (see \secref{sec:class}) provide a way to introduce proven class
    1.23    relations.
    1.24  
    1.25 -  \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
    1.26 +  \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}~\isa{s} makes sort \isa{s} the
    1.27    new default sort for any type variable that is given explicitly in
    1.28    the text, but lacks a sort constraint (wrt.\ the current context).
    1.29    Type variables generated by type inference are not affected.