Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export ML function (towards nonuniform datatypes)
authorblanchet
Wed, 21 Dec 2016 13:35:58 +0100
changeset 64628 19bc22274cd9
parent 64627 8d7cb22482e3
child 64629 a331208010b6
export ML function (towards nonuniform datatypes)
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Dec 21 12:49:15 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Dec 21 13:35:58 2016 +0100
@@ -28,6 +28,8 @@
   val mk_disc_transfer_tac: Proof.context -> thm -> thm -> thm list -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
+  val mk_induct_discharge_prem_tac: Proof.context -> int -> int -> thm list -> thm list ->
+    thm list -> thm list -> int -> int -> int list -> tactic
   val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
     thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
isabelle