1(*
2 * Copyright 1991-1995  University of Cambridge (Author: Monica Nesi)
3 * Copyright 2016-2017  University of Bologna   (Author: Chun Tian)
4 *)
5
6signature CCSLib =
7sig
8  include Abbrev
9
10  val PAT_X_ASSUM               : term -> thm_tactic -> tactic
11  val qpat_x_assum              : Q.tmquote -> thm_tactic -> tactic
12  val Q_GENL                    : Q.tmquote list -> thm -> thm
13  val fix                       : Q.tmquote list -> tactic
14  val set                       : Q.tmquote list -> tactic
15  val take                      : Q.tmquote list -> tactic
16  val Know                      : Q.tmquote -> tactic
17  val Suff                      : Q.tmquote -> tactic
18  val K_TAC                     : 'a -> tactic
19  val KILL_TAC                  : tactic
20  val wrap                      : 'a -> 'a list
21  val art                       : thm list -> tactic
22  val Rewr                      : tactic
23  val Rewr'                     : tactic
24  val Rev                       : tactic -> tactic
25  val PRINT_TAC                 : string -> tactic
26  val COUNT_TAC                 : tactic -> tactic
27  val STRONG_CONJ_TAC           : tactic
28  val X_TAC                     : int -> tactic
29
30  val ONCE_REWRITE_RHS_RULE     : thm list -> thm -> thm
31  val PURE_REWRITE_RHS_RULE     : thm list -> thm -> thm
32  val REWRITE_RHS_RULE          : thm list -> thm -> thm
33  val ONCE_REWRITE_RHS_TAC      : thm list -> tactic
34  val REWRITE_RHS_TAC           : thm list -> tactic
35  val ONCE_REWRITE_LHS_RULE     : thm list -> thm -> thm
36  val PURE_REWRITE_LHS_RULE     : thm list -> thm -> thm
37  val REWRITE_LHS_RULE          : thm list -> thm -> thm
38  val ONCE_REWRITE_LHS_TAC      : thm list -> tactic
39  val REWRITE_LHS_TAC           : thm list -> tactic
40  val ONCE_ASM_REWRITE_LHS_RULE : thm list -> thm -> thm
41  val ONCE_ASM_REWRITE_LHS_TAC  : thm list -> tactic
42  val SWAP_FORALL_CONV          : term -> thm
43  val STRIP_FORALL_RULE         : (thm -> thm) -> thm -> thm
44  val EQ_IMP_LR                 : thm -> thm
45  val EQ_IMP_RL                 : thm -> thm
46  val lconcl                    : thm -> term
47  val rconcl                    : thm -> term
48
49  val args_thm                  : thm -> term * term
50  val lhs_tm                    : thm -> term
51  val rhs_tm                    : thm -> term
52  val args_equiv                : term -> term * term * term
53  val elim                      : term -> term list -> term list
54  val list_apply_tac            : ('a -> tactic) -> 'a list -> tactic list
55
56end
57
58(* last updated: May 14, 2017 *)
59