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