src/Pure/Isar/isar_syn.ML

 
 (* classes and sorts *)
 
 val classesP =
   OuterSyntax.command "classes" "declare type classes" K.thy_decl
-    (Scan.repeat1 (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [])
+    (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+        P.!!! (P.list1 P.xname)) [])
       -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes));
 
 val classrelP =
   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
-    (P.xname -- (P.$$$ "<" |-- P.!!! P.xname) -- P.marg_comment
+    (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) -- P.marg_comment
       >> (Toplevel.theory o IsarThy.add_classrel));
 
 val defaultsortP =
   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort));

 
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
   "files", "in", "infixl", "infixr", "is", "output", "overloaded",
-  "|", "\\<rightharpoonup>", "\\<leftharpoondown>",
-  "\\<rightleftharpoons>", "\\<equiv>"];
+  "|", "\\<equiv>", "\\<rightharpoonup>", "\\<leftharpoondown>",
+  "\\<rightleftharpoons>", "\\<subseteq>"];
 
 val parsers = [
   (*theory structure*)
   theoryP, end_excursionP, contextP,
   (*markup commands*)