equal
deleted
inserted
replaced
25 val atac: int -> tactic |
25 val atac: int -> tactic |
26 val rtac: thm -> int -> tactic |
26 val rtac: thm -> int -> tactic |
27 val dtac: thm -> int -> tactic |
27 val dtac: thm -> int -> tactic |
28 val etac: thm -> int -> tactic |
28 val etac: thm -> int -> tactic |
29 val ftac: thm -> int -> tactic |
29 val ftac: thm -> int -> tactic |
30 val ares_tac: thm list -> int -> tactic |
30 val ares_tac: Proof.context -> thm list -> int -> tactic |
31 val solve_tac: Proof.context -> thm list -> int -> tactic |
31 val solve_tac: Proof.context -> thm list -> int -> tactic |
32 val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic |
32 val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic |
33 val match_tac: Proof.context -> thm list -> int -> tactic |
33 val match_tac: Proof.context -> thm list -> int -> tactic |
34 val ematch_tac: Proof.context -> thm list -> int -> tactic |
34 val ematch_tac: Proof.context -> thm list -> int -> tactic |
35 val dmatch_tac: Proof.context -> thm list -> int -> tactic |
35 val dmatch_tac: Proof.context -> thm list -> int -> tactic |
142 fun rtac rl = resolve0_tac [rl]; |
142 fun rtac rl = resolve0_tac [rl]; |
143 fun dtac rl = dresolve0_tac [rl]; |
143 fun dtac rl = dresolve0_tac [rl]; |
144 fun etac rl = eresolve0_tac [rl]; |
144 fun etac rl = eresolve0_tac [rl]; |
145 fun ftac rl = forward0_tac [rl]; |
145 fun ftac rl = forward0_tac [rl]; |
146 |
146 |
147 (*Use an assumption or some rules ... A popular combination!*) |
147 (*Use an assumption or some rules*) |
148 fun ares_tac rules = atac ORELSE' resolve0_tac rules; |
148 fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules; |
149 |
149 |
150 fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt; |
150 fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt; |
151 |
151 |
152 (*Matching tactics -- as above, but forbid updating of state*) |
152 (*Matching tactics -- as above, but forbid updating of state*) |
153 fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i); |
153 fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i); |