1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 17:48:05 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 18:10:37 2010 +0100
     1.3 @@ -973,13 +973,13 @@
     1.4  
     1.5  text {*
     1.6    \begin{matharray}{rcll}
     1.7 -    @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.8 +    @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.9      @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    1.10      @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    1.11    \end{matharray}
    1.12  
    1.13    \begin{rail}
    1.14 -    'types' (typespec '=' type mixfix? +)
    1.15 +    'type_synonym' (typespec '=' type mixfix?)
    1.16      ;
    1.17      'typedecl' typespec mixfix?
    1.18      ;
    1.19 @@ -989,12 +989,12 @@
    1.20  
    1.21    \begin{description}
    1.22  
    1.23 -  \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
    1.24 -  \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
    1.25 -  @{text "\<tau>"}.  Unlike actual type definitions, as are available in
    1.26 -  Isabelle/HOL for example, type synonyms are merely syntactic
    1.27 -  abbreviations without any logical significance.  Internally, type
    1.28 -  synonyms are fully expanded.
    1.29 +  \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}
    1.30 +  introduces a \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the
    1.31 +  existing type @{text "\<tau>"}.  Unlike actual type definitions, as are
    1.32 +  available in Isabelle/HOL for example, type synonyms are merely
    1.33 +  syntactic abbreviations without any logical significance.
    1.34 +  Internally, type synonyms are fully expanded.
    1.35    
    1.36    \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
    1.37    type constructor @{text t}.  If the object-logic defines a base sort