src/Pure/axclass.ML
changeset 11101 014e7b5c77ba
parent 10507 ea5de7c64c23
child 11353 7f6eff7bc97a
     1.1 --- a/src/Pure/axclass.ML	Mon Feb 12 20:44:02 2001 +0100
     1.2 +++ b/src/Pure/axclass.ML	Mon Feb 12 20:45:12 2001 +0100
     1.3 @@ -465,13 +465,15 @@
     1.4  
     1.5  val axclassP =
     1.6    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     1.7 -    (((P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
     1.8 +    (((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     1.9 +        P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
    1.10        -- Scan.repeat (P.spec_name --| P.marg_comment)
    1.11        >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
    1.12  
    1.13  val instanceP =
    1.14    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    1.15 -    ((P.xname -- (P.$$$ "<" |-- P.xname) -- P.marg_comment >> instance_subclass_proof ||
    1.16 +    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname)
    1.17 +        -- P.marg_comment >> instance_subclass_proof ||
    1.18        (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment
    1.19          >> instance_arity_proof)
    1.20        >> (Toplevel.print oo Toplevel.theory_to_proof));