src/HOL/Tools/specification_package.ML
changeset 24867 e5b55d7be9bb
parent 24707 dfeb98f84e93
child 26478 9d1029ce0e13
     1.1 --- a/src/HOL/Tools/specification_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/specification_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
     1.5            Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
     1.6  
     1.7 -val specificationP =
     1.8 +val _ =
     1.9    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
    1.10      (specification_decl >> (fn (cos,alt_props) =>
    1.11                                 Toplevel.print o (Toplevel.theory_to_proof
    1.12 @@ -255,14 +255,12 @@
    1.13      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    1.14             Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
    1.15  
    1.16 -val ax_specificationP =
    1.17 +val _ =
    1.18    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
    1.19      (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
    1.20                                 Toplevel.print o (Toplevel.theory_to_proof
    1.21                                                       (process_spec (SOME axname) cos alt_props))))
    1.22  
    1.23 -val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP]
    1.24 -
    1.25  end
    1.26  
    1.27