src/HOL/Tools/specification_package.ML
changeset 22101 6d13239d5f52
parent 21858 05f57309170c
child 22578 b0eb5652f210
equal deleted inserted replaced
22100:33d7468302bb 22101:6d13239d5f52
   239 val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
   239 val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
   240 val opt_overloaded = P.opt_keyword "overloaded";
   240 val opt_overloaded = P.opt_keyword "overloaded";
   241 
   241 
   242 val specification_decl =
   242 val specification_decl =
   243   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   243   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   244           Scan.repeat1 (P.opt_thm_name ":" -- P.prop)
   244           Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
   245 
   245 
   246 val specificationP =
   246 val specificationP =
   247   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   247   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   248     (specification_decl >> (fn (cos,alt_props) =>
   248     (specification_decl >> (fn (cos,alt_props) =>
   249                                Toplevel.print o (Toplevel.theory_to_proof
   249                                Toplevel.print o (Toplevel.theory_to_proof
   250                                                      (process_spec NONE cos alt_props))))
   250                                                      (process_spec NONE cos alt_props))))
   251 
   251 
   252 val ax_specification_decl =
   252 val ax_specification_decl =
   253     P.name --
   253     P.name --
   254     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   254     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   255            Scan.repeat1 (P.opt_thm_name ":" -- P.prop))
   255            Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
   256 
   256 
   257 val ax_specificationP =
   257 val ax_specificationP =
   258   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
   258   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
   259     (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
   259     (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
   260                                Toplevel.print o (Toplevel.theory_to_proof
   260                                Toplevel.print o (Toplevel.theory_to_proof