export ML function (towards nonuniform datatypes)
authorblanchet
Wed Dec 21 13:35:58 2016 +0100 (2016-12-21)
changeset 6462819bc22274cd9
parent 64627 8d7cb22482e3
child 64629 a331208010b6
export ML function (towards nonuniform datatypes)
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Dec 21 12:49:15 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Dec 21 13:35:58 2016 +0100
     1.3 @@ -28,6 +28,8 @@
     1.4    val mk_disc_transfer_tac: Proof.context -> thm -> thm -> thm list -> tactic
     1.5    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
     1.6    val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
     1.7 +  val mk_induct_discharge_prem_tac: Proof.context -> int -> int -> thm list -> thm list ->
     1.8 +    thm list -> thm list -> int -> int -> int list -> tactic
     1.9    val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
    1.10      thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
    1.11    val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic