equal
deleted
inserted
replaced
90 (P.sort >> (Toplevel.theory o Theory.add_defsort)); |
90 (P.sort >> (Toplevel.theory o Theory.add_defsort)); |
91 |
91 |
92 val axclassP = |
92 val axclassP = |
93 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
93 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
94 ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
94 ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
95 P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name |
95 P.!!! (P.list1 P.xname)) []) -- |
|
96 Scan.repeat (P.thm_name ":" -- (P.prop >> single)) |
96 >> (fn (x, y) => Toplevel.theory (snd o AxClass.add_axclass x [] y))); |
97 >> (fn (x, y) => Toplevel.theory (snd o AxClass.add_axclass x [] y))); |
97 |
98 |
98 |
99 |
99 (* types *) |
100 (* types *) |
100 |
101 |