1signature Q =
2sig
3  include Abbrev
4  type tmquote = term quotation
5  type tyquote = hol_type quotation
6
7  val REFL                   : tmquote -> thm
8  val ABS                    : tmquote -> thm -> thm
9  val AC_CONV                : thm * thm -> tmquote -> thm
10  val AP_TERM                : tmquote -> thm -> thm
11  val AP_THM                 : thm -> tmquote -> thm
12  val ASM_CASES_TAC          : tmquote -> tactic
13  val ASSUME                 : tmquote -> thm
14  val BETA_CONV              : tmquote -> thm
15  val DISJ1                  : thm -> tmquote -> thm
16  val DISJ2                  : tmquote -> thm -> thm
17  val EXISTS                 : tmquote * tmquote -> thm -> thm
18  val EXISTS_TAC             : tmquote -> tactic
19  val LIST_EXISTS_TAC        : tmquote list -> tactic
20  val REFINE_EXISTS_TAC      : tmquote -> tactic
21  val GEN                    : tmquote -> thm -> thm
22  val GENL                   : tmquote list -> thm -> thm
23  val SPEC                   : tmquote -> thm -> thm
24  val ID_SPEC                : thm -> thm
25  val SPECL                  : tmquote list -> thm -> thm
26  val ISPEC                  : tmquote -> thm -> thm
27  val ISPECL                 : tmquote list -> thm -> thm
28  val SPEC_TAC               : tmquote * tmquote -> tactic
29  val SPEC_THEN              : tmquote -> thm_tactic -> thm -> tactic
30  val SPECL_THEN             : tmquote list -> thm_tactic -> thm -> tactic
31  val ISPEC_THEN             : tmquote -> thm_tactic -> thm -> tactic
32  val ISPECL_THEN            : tmquote list -> thm_tactic -> thm ->tactic
33  val ID_SPEC_TAC            : tmquote -> tactic
34  val SUBGOAL_THEN           : tmquote -> thm_tactic -> tactic
35  val DISCH                  : tmquote -> thm -> thm
36  val PAT_UNDISCH_TAC        : tmquote -> tactic
37  val hdtm_assum             : tmquote -> thm_tactic -> tactic
38  val hdtm_x_assum           : tmquote -> thm_tactic -> tactic
39  val UNDISCH_THEN           : tmquote -> thm_tactic -> tactic
40  val PAT_ASSUM              : tmquote -> thm_tactic -> tactic
41  val PAT_X_ASSUM            : tmquote -> thm_tactic -> tactic
42  val UNDISCH_TAC            : tmquote -> tactic
43  val X_CHOOSE_TAC           : tmquote -> thm_tactic
44  val X_CHOOSE_THEN          : tmquote -> thm_tactic -> thm_tactic
45  val X_GEN_TAC              : tmquote -> tactic
46  val X_FUN_EQ_CONV          : tmquote -> conv
47  val X_SKOLEM_CONV          : tmquote -> conv
48  val store_thm              : string * tmquote * tactic -> thm
49  val prove                  : tmquote * tactic -> thm
50  val INST                   : (tmquote, tmquote) subst -> thm -> thm
51  val new_definition         : string * tmquote -> thm
52  val new_infixl_definition  : string * tmquote * int -> thm
53  val new_infixr_definition  : string * tmquote * int -> thm
54  val INST_TYPE              : (tyquote, tyquote) subst -> thm -> thm
55
56  val ABBREV_TAC             : tmquote -> tactic
57  val PAT_ABBREV_TAC         : tmquote -> tactic
58  val MATCH_ABBREV_TAC       : tmquote -> tactic
59  val MATCH_ASSUM_ABBREV_TAC : tmquote -> tactic
60  val HO_MATCH_ABBREV_TAC    : tmquote -> tactic
61  val UNABBREV_TAC           : tmquote -> tactic
62  val RM_ABBREV_TAC          : tmquote -> tactic
63
64  val MATCH_RENAME_TAC       : tmquote -> tactic
65  val MATCH_ASSUM_RENAME_TAC : tmquote -> tactic
66  val MATCH_GOALSUB_RENAME_TAC : tmquote -> tactic
67  val MATCH_ASMSUB_RENAME_TAC : tmquote -> tactic
68  val MATCH_GOALSUB_ABBREV_TAC : tmquote -> tactic
69  val MATCH_ASMSUB_ABBREV_TAC : tmquote -> tactic
70  val RENAME1_TAC            : tmquote -> tactic
71  val RENAME_TAC             : tmquote list -> tactic
72  val kRENAME_TAC            : tmquote list -> tactic -> tactic
73  val coreRENAME_TAC         : tmquote list -> tactic -> tactic
74
75end
76