src/HOL/Tools/specification_package.ML
changeset 14118 05416ba8eef2
parent 14117 d3512dedbaea
child 14121 d2a0fd183f5f
equal deleted inserted replaced
14117:d3512dedbaea 14118:05416ba8eef2
     7 *)
     7 *)
     8 
     8 
     9 signature SPECIFICATION_PACKAGE =
     9 signature SPECIFICATION_PACKAGE =
    10 sig
    10 sig
    11     val quiet_mode: bool ref
    11     val quiet_mode: bool ref
    12     val add_specification: (bstring * bstring * bool) list -> bstring * Args.src list
    12     val add_specification: (bstring * xstring * bool) list -> bstring * Args.src list
    13 			   -> theory * thm -> theory * thm
    13 			   -> theory * thm -> theory * thm
    14     val add_specification_i: (bstring * bstring * bool) list -> bstring * theory attribute list
    14     val add_specification_i: (bstring * xstring * bool) list -> bstring * theory attribute list
    15 			     -> theory * thm -> theory * thm
    15 			     -> theory * thm -> theory * thm
    16 end
    16 end
    17 
    17 
    18 structure SpecificationPackage : SPECIFICATION_PACKAGE =
    18 structure SpecificationPackage : SPECIFICATION_PACKAGE =
    19 struct
    19 struct