diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -932,7 +932,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
+    @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \<newline>
       (@{syntax type} '+')? (constdecl +)
     ;
     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
@@ -1131,7 +1131,9 @@
   definition, but less powerful in practice.
 
   @{rail \<open>
-    @@{command (HOL) typedef} abs_type '=' rep_set
+    @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
+    ;
+    @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
     ;
     abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
     ;
@@ -1185,6 +1187,13 @@
   for the generic @{method cases} and @{method induct} methods,
   respectively.
 
+  \medskip The ``@{text "(overloaded)"}'' option allows the @{command
+  "typedef"} specification to depend on constants that are not (yet)
+  specified and thus left open as parameters. In particular, a @{command
+  typedef} depending on type-class parameters (cf.\ \secref{sec:class}) is
+  semantically like a dependent type: its meaning is determined for
+  different type-class instances according to their respective operations.
+
   \end{description}
 \<close>
 
@@ -1299,8 +1308,9 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '='
-      quot_type \<newline> quot_morphisms? quot_parametric?
+    @@{command (HOL) quotient_type} @{syntax "overloaded"}? \<newline>
+      @{syntax typespec} @{syntax mixfix}? '=' quot_type \<newline>
+      quot_morphisms? quot_parametric?
     ;
     quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
     ;