
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 \<rightarrow> local_theory"} \\
+    @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "arities"} & : & @{text "theory \<rightarrow> 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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
-  \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
-  @{text "\<tau>"}.  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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}
+  introduces a \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the
+  existing type @{text "\<tau>"}.  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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
   type constructor @{text t}.  If the object-logic defines a base sort




