1.1 --- a/NEWS	Wed Apr 28 12:18:49 2010 +0200
     1.2 +++ b/NEWS	Wed Apr 28 12:21:55 2010 +0200
     1.3 @@ -116,6 +116,9 @@
     1.4  context -- without introducing dependencies on parameters or
     1.5  assumptions, which is not possible in Isabelle/Pure.
     1.6  
     1.7 +* Command 'defaultsort' is renamed to 'default_sort', it works within
     1.8 +a local theory context.  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Proof terms: Type substitutions on proof constants now use canonical
    1.11  order of type variables. INCOMPATIBILITY: Tools working with proof
    1.12  terms may need to be adapted.

     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Apr 28 12:18:49 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Apr 28 12:21:55 2010 +0200
     2.3 @@ -902,7 +902,7 @@
     2.4    \begin{matharray}{rcll}
     2.5      @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
     2.6      @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
     2.7 -    @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8 +    @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.9      @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.10    \end{matharray}
    2.11  
    2.12 @@ -911,7 +911,7 @@
    2.13      ;
    2.14      'classrel' (nameref ('<' | subseteq) nameref + 'and')
    2.15      ;
    2.16 -    'defaultsort' sort
    2.17 +    'default\_sort' sort
    2.18      ;
    2.19    \end{rail}
    2.20  
    2.21 @@ -929,7 +929,7 @@
    2.22    (see \secref{sec:class}) provide a way to introduce proven class
    2.23    relations.
    2.24  
    2.25 -  \item @{command "defaultsort"}~@{text s} makes sort @{text s} the
    2.26 +  \item @{command "default_sort"}~@{text s} makes sort @{text s} the
    2.27    new default sort for any type variable that is given explicitly in
    2.28    the text, but lacks a sort constraint (wrt.\ the current context).
    2.29    Type variables generated by type inference are not affected.

     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Apr 28 12:18:49 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Apr 28 12:21:55 2010 +0200
     3.3 @@ -937,7 +937,7 @@
     3.4  \begin{matharray}{rcll}
     3.5      \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.6      \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
     3.7 -    \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.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}} \\
     3.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}} \\
    3.10    \end{matharray}
    3.11  
    3.12 @@ -946,7 +946,7 @@
    3.13      ;
    3.14      'classrel' (nameref ('<' | subseteq) nameref + 'and')
    3.15      ;
    3.16 -    'defaultsort' sort
    3.17 +    'default\_sort' sort
    3.18      ;
    3.19    \end{rail}
    3.20  
    3.21 @@ -964,7 +964,7 @@
    3.22    (see \secref{sec:class}) provide a way to introduce proven class
    3.23    relations.
    3.24  
    3.25 -  \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
    3.26 +  \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}~\isa{s} makes sort \isa{s} the
    3.27    new default sort for any type variable that is given explicitly in
    3.28    the text, but lacks a sort constraint (wrt.\ the current context).
    3.29    Type variables generated by type inference are not affected.