equal
deleted
inserted
replaced
360 |
360 |
361 |
361 |
362 |
362 |
363 (** outer syntax **) |
363 (** outer syntax **) |
364 |
364 |
365 local structure P = OuterParse and K = OuterSyntax.Keyword in |
365 local structure P = OuterParse and K = OuterKeyword in |
366 |
366 |
367 val axclassP = |
367 val axclassP = |
368 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
368 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
369 ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
369 ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
370 P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name |
370 P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name |