diff -r 8d966b4a7469 -r df85956228c2 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Jul 03 09:57:26 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Jul 03 13:51:55 2017 +0200
@@ -1311,6 +1311,8 @@
 
 text \<open>
   \begin{matharray}{rcl}
+    @{command_def "alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command_def "type_alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\
@@ -1318,8 +1320,10 @@
   \end{matharray}
 
   @{rail \<open>
-    ( @{command hide_class} | @{command hide_type} |
-      @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + )
+    (@{command alias} | @{command type_alias}) @{syntax name} '=' @{syntax name}
+    ;
+    (@{command hide_class} | @{command hide_type} |
+      @{command hide_const} | @{command hide_fact}) ('(' @'open' ')')? (@{syntax name} + )
   \<close>}
 
   Isabelle organizes any kind of name declarations (of types, constants,
@@ -1327,6 +1331,12 @@
   the user does not have to control the behaviour of name spaces by hand, yet
   the following commands provide some way to do so.
 
+  \<^descr> \<^theory_text>\<open>alias\<close> and \<^theory_text>\<open>type_alias\<close> introduce aliases for constants and type
+  constructors, respectively. This allows adhoc changes to name-space
+  accesses.
+
+  \<^descr> \<^theory_text>\<open>type_alias b = c\<close> introduces an alias for an existing type constructor.
+
   \<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name
   space; with the \<open>(open)\<close> option, only the unqualified base name is hidden.