--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Dec 16 22:54:14 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Dec 20 16:17:13 2016 +0100
@@ -10,6 +10,7 @@
sig
val sumprod_thms_rel: thm list
+ val co_induct_inst_as_projs_tac: Proof.context -> int -> tactic
val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic
val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->