diff -r b301d1f72552 -r 34d58b1818f4 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Feb 12 20:43:12 2001 +0100
+++ b/doc-src/IsarRef/syntax.tex	Mon Feb 12 20:44:02 2001 +0100
@@ -159,10 +159,13 @@
 referring to the intersection of these classes.  The syntax of type arities is
 given directly at the outer level.
 
+\railalias{subseteq}{\isasymsubseteq}
+\railterm{subseteq}
+
 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
 \indexouternonterm{classdecl}
 \begin{rail}
-  classdecl: name ('<' (nameref + ','))?
+  classdecl: name (('<' | subseteq) (nameref + ','))?
   ;
   sort: nameref
   ;