equal
deleted
inserted
replaced
26 val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic |
26 val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic |
27 val match_tac: Proof.context -> thm list -> int -> tactic |
27 val match_tac: Proof.context -> thm list -> int -> tactic |
28 val ematch_tac: Proof.context -> thm list -> int -> tactic |
28 val ematch_tac: Proof.context -> thm list -> int -> tactic |
29 val dmatch_tac: Proof.context -> thm list -> int -> tactic |
29 val dmatch_tac: Proof.context -> thm list -> int -> tactic |
30 val flexflex_tac: Proof.context -> tactic |
30 val flexflex_tac: Proof.context -> tactic |
31 val distinct_subgoal_tac: int -> tactic |
|
32 val distinct_subgoals_tac: tactic |
31 val distinct_subgoals_tac: tactic |
33 val cut_tac: thm -> int -> tactic |
32 val cut_tac: thm -> int -> tactic |
34 val cut_rules_tac: thm list -> int -> tactic |
33 val cut_rules_tac: thm list -> int -> tactic |
35 val cut_facts_tac: thm list -> int -> tactic |
34 val cut_facts_tac: thm list -> int -> tactic |
36 val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list |
35 val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list |