equal
deleted
inserted
replaced
425 |
425 |
426 (* classes *) |
426 (* classes *) |
427 |
427 |
428 val class_val = |
428 val class_val = |
429 SpecParse.class_expr -- |
429 SpecParse.class_expr -- |
430 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.locale_element)) [] || |
430 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
431 Scan.repeat1 SpecParse.locale_element >> pair []; |
431 Scan.repeat1 SpecParse.context_element >> pair []; |
432 |
432 |
433 val _ = |
433 val _ = |
434 OuterSyntax.command "class" "define type class" K.thy_decl |
434 OuterSyntax.command "class" "define type class" K.thy_decl |
435 (P.name -- |
435 (P.name -- |
436 Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] -- (* FIXME ?? *) |
436 Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] -- (* FIXME ?? *) |