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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
