[isabelle-dev] Exposing some functions of the API

[Frédéric Tuong]

Dear all,

During some programming tasks, I had to use the following functions:

BNF_FP_Def_Sugar.co_datatype_cmd
Classical.rule_tac
Metis_Tactic.metis_method

However they only appear inside their respective structures, would it be 
possible to write their corresponding types in signatures, at least for 
some of them?

The current solution I found was to copy-paste elsewhere these functions 
without their signatures, but more spaces could perhaps be saved...

Thanks,
Frédéric


PS: Here are their locations and types:

(* src/HOL/Tools/BNF/bnf_fp_def_sugar.ML *)
val co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> 
binding list ->
       binding list list -> binding list -> (string * sort) list -> typ 
list * typ list list ->
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
       BNF_FP_Util.fp_result * local_theory) ->
     Ctr_Sugar.ctr_options_cmd
     * ((((((binding option * (string * string option)) list * binding) 
* mixfix)
          * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) 
list) * (binding * binding))
        * string list) list ->
     local_theory -> local_theory

(* src/Provers/classical.ML *)
val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic

(* src/HOL/Tools/Metis/metis_tactic.ML *)
val metis_method :
      (string list option * string option) * thm list -> Proof.context 
-> thm list -> thm -> thm Seq.seq