diff -r 7cf837f1a8df -r 26f12f98f50a doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Fri Dec 17 17:48:05 2010 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Fri Dec 17 18:10:37 2010 +0100 @@ -973,13 +973,13 @@ text {* \begin{matharray}{rcll} - @{command_def "types"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "type_synonym"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "typedecl"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} \begin{rail} - 'types' (typespec '=' type mixfix? +) + 'type_synonym' (typespec '=' type mixfix?) ; 'typedecl' typespec mixfix? ; @@ -989,12 +989,12 @@ \begin{description} - \item @{command "types"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} introduces a - \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the existing type - @{text "\"}. Unlike actual type definitions, as are available in - Isabelle/HOL for example, type synonyms are merely syntactic - abbreviations without any logical significance. Internally, type - synonyms are fully expanded. + \item @{command "type_synonym"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} + introduces a \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the + existing type @{text "\"}. Unlike actual type definitions, as are + available in Isabelle/HOL for example, type synonyms are merely + syntactic abbreviations without any logical significance. + Internally, type synonyms are fully expanded. \item @{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} declares a new type constructor @{text t}. If the object-logic defines a base sort