230 val opt_name = Scan.optional (P.name --| P.$$$ ":") "" |
230 val opt_name = Scan.optional (P.name --| P.$$$ ":") "" |
231 val opt_overloaded = P.opt_keyword "overloaded"; |
231 val opt_overloaded = P.opt_keyword "overloaded"; |
232 |
232 |
233 val specification_decl = |
233 val specification_decl = |
234 P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- |
234 P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- |
235 Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop) |
235 Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop) |
236 |
236 |
237 val _ = |
237 val _ = |
238 OuterSyntax.command "specification" "define constants by specification" K.thy_goal |
238 OuterSyntax.command "specification" "define constants by specification" K.thy_goal |
239 (specification_decl >> (fn (cos,alt_props) => |
239 (specification_decl >> (fn (cos,alt_props) => |
240 Toplevel.print o (Toplevel.theory_to_proof |
240 Toplevel.print o (Toplevel.theory_to_proof |
241 (process_spec NONE cos alt_props)))) |
241 (process_spec NONE cos alt_props)))) |
242 |
242 |
243 val ax_specification_decl = |
243 val ax_specification_decl = |
244 P.name -- |
244 P.name -- |
245 (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- |
245 (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- |
246 Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)) |
246 Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)) |
247 |
247 |
248 val _ = |
248 val _ = |
249 OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal |
249 OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal |
250 (ax_specification_decl >> (fn (axname,(cos,alt_props)) => |
250 (ax_specification_decl >> (fn (axname,(cos,alt_props)) => |
251 Toplevel.print o (Toplevel.theory_to_proof |
251 Toplevel.print o (Toplevel.theory_to_proof |