blob: e12ed0e8ca8c1b720669d9c3dbed425ced3eb9dd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
(*i $Id$ i*)
(*i*)
open Proof_type
open Tacmach
(*i*)
(* Registered tactics. *)
val v_absurd : tactic_arg list -> tactic
val v_contradiction : tactic_arg list -> tactic
val v_reflexivity : tactic_arg list -> tactic
val v_symmetry : tactic_arg list -> tactic
val v_transitivity : tactic_arg list -> tactic
val v_intro : tactic_arg list -> tactic
val v_introsUntil : tactic_arg list -> tactic
(*i val v_tclIDTAC : tactic_arg list -> tactic i*)
val v_assumption : tactic_arg list -> tactic
val v_exact : tactic_arg list -> tactic
val v_reduce : tactic_arg list -> tactic
val v_constructor : tactic_arg list -> tactic
val v_left : tactic_arg list -> tactic
val v_right : tactic_arg list -> tactic
val v_split : tactic_arg list -> tactic
val v_clear : tactic_arg list -> tactic
val v_move : tactic_arg list -> tactic
val v_move_dep : tactic_arg list -> tactic
val v_apply : tactic_arg list -> tactic
val v_cutAndResolve : tactic_arg list -> tactic
val v_cut : tactic_arg list -> tactic
val v_lettac : tactic_arg list -> tactic
val v_generalize : tactic_arg list -> tactic
val v_generalize_dep : tactic_arg list -> tactic
val v_specialize : tactic_arg list -> tactic
val v_elim : tactic_arg list -> tactic
val v_elimType : tactic_arg list -> tactic
val v_induction : tactic_arg list -> tactic
val v_case : tactic_arg list -> tactic
val v_caseType : tactic_arg list -> tactic
val v_destruct : tactic_arg list -> tactic
val v_fix : tactic_arg list -> tactic
val v_cofix : tactic_arg list -> tactic
|
