equal
deleted
inserted
replaced
193 |
193 |
194 (* constant specifications *) |
194 (* constant specifications *) |
195 |
195 |
196 val axiomatizationP = |
196 val axiomatizationP = |
197 OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl |
197 OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl |
198 (P.fixes -- Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) [] |
198 (P.opt_locale_target -- |
199 >> (Toplevel.theory o (#2 oo Specification.axiomatize))); |
199 Scan.optional P.fixes [] -- |
|
200 Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) [] |
|
201 >> (fn ((x, y), z) => Toplevel.theory_context (#2 o Specification.axiomatization x y z))); |
200 |
202 |
201 |
203 |
202 (* theorems *) |
204 (* theorems *) |
203 |
205 |
204 fun theorems kind = P.opt_locale_target -- P.name_facts |
206 fun theorems kind = P.opt_locale_target -- P.name_facts |