# HG changeset patch
# User wenzelm
# Date 982007112 -3600
# Node ID 014e7b5c77ba38ea8e3a42badc317752dcb83b1a
# Parent  34d58b1818f4c0f2d6f8916b87ae5b22c1c96ac1
support \<subseteq> syntax in classes/classrel/axclass/instance;

diff -r 34d58b1818f4 -r 014e7b5c77ba src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Feb 12 20:44:02 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Feb 12 20:45:12 2001 +0100
@@ -85,12 +85,13 @@
 
 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 =
@@ -668,8 +669,8 @@
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
   "files", "in", "infixl", "infixr", "is", "output", "overloaded",
-  "|", "\\<rightharpoonup>", "\\<leftharpoondown>",
-  "\\<rightleftharpoons>", "\\<equiv>"];
+  "|", "\\<equiv>", "\\<rightharpoonup>", "\\<leftharpoondown>",
+  "\\<rightleftharpoons>", "\\<subseteq>"];
 
 val parsers = [
   (*theory structure*)
diff -r 34d58b1818f4 -r 014e7b5c77ba src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Feb 12 20:44:02 2001 +0100
+++ b/src/Pure/axclass.ML	Mon Feb 12 20:45:12 2001 +0100
@@ -465,13 +465,15 @@
 
 val axclassP =
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
-    (((P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
+    (((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+        P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
       -- Scan.repeat (P.spec_name --| P.marg_comment)
       >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
 
 val instanceP =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
-    ((P.xname -- (P.$$$ "<" |-- P.xname) -- P.marg_comment >> instance_subclass_proof ||
+    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname)
+        -- P.marg_comment >> instance_subclass_proof ||
       (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment
         >> instance_arity_proof)
       >> (Toplevel.print oo Toplevel.theory_to_proof));