equal
deleted
inserted
replaced
8 |
8 |
9 signature BNF_FP_DEF_SUGAR_TACTICS = |
9 signature BNF_FP_DEF_SUGAR_TACTICS = |
10 sig |
10 sig |
11 val sumprod_thms_rel: thm list |
11 val sumprod_thms_rel: thm list |
12 |
12 |
|
13 val co_induct_inst_as_projs_tac: Proof.context -> int -> tactic |
13 val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic |
14 val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic |
14 val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> |
15 val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> |
15 thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> |
16 thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> |
16 thm list list list -> tactic |
17 thm list list list -> tactic |
17 val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic |
18 val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic |