1signature Tactical = 2sig 3 include Abbrev 4 5 val TAC_PROOF : goal * tactic -> thm 6 val prove : term * tactic -> thm 7 val store_thm : string * term * tactic -> thm 8 val CONV_TAC : conv -> tactic 9 val THEN : ('a,'b) gentactic * tactic -> ('a,'b) gentactic 10 val >> : ('a,'b) gentactic * tactic -> ('a,'b) gentactic 11 val \\ : ('a,'b) gentactic * tactic -> ('a,'b) gentactic 12 (* could be used as 13 val THEN : tactic * tactic -> tactic 14 val THEN : list_tactic * tactic -> list_tactic 15 *) 16 val THENL : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic 17 val >| : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic 18 (* could be used as 19 val THENL : tactic * tactic list -> tactic 20 val THENL : list_tactic * tactic list -> list_tactic 21 *) 22 val ORELSE : tactic * tactic -> tactic 23 val ORELSE_LT : list_tactic * list_tactic -> list_tactic 24 val THEN1 : tactic * tactic -> tactic 25 val >- : tactic * tactic -> tactic 26 val THEN_LT : ('a,'b) gentactic * list_tactic -> ('a,'b) gentactic 27 val >>> : ('a,'b) gentactic * list_tactic -> ('a,'b) gentactic 28 (* could be used as 29 val THEN_LT : tactic * list_tactic -> tactic 30 val THEN_LT : list_tactic * list_tactic -> list_tactic 31 *) 32 val >>- : tactic * int -> tactic -> tactic 33 val ?? : ('a -> 'b) * 'a -> 'b 34 val TACS_TO_LT : tactic list -> list_tactic 35 val NULL_OK_LT : list_tactic -> list_tactic 36 val ALLGOALS : tactic -> list_tactic 37 val TRYALL : tactic -> list_tactic 38 val NTH_GOAL : tactic -> int -> list_tactic 39 val LASTGOAL : tactic -> list_tactic 40 val HEADGOAL : tactic -> list_tactic 41 val SPLIT_LT : int -> list_tactic * list_tactic -> list_tactic 42 val ROTATE_LT : int -> list_tactic 43 val REVERSE : tactic -> tactic 44 val reverse : tactic -> tactic 45 val REVERSE_LT : list_tactic 46 val FAIL_TAC : string -> tactic 47 val NO_TAC : tactic 48 val FAIL_LT : string -> list_tactic 49 val NO_LT : list_tactic 50 val ALL_TAC : tactic 51 val all_tac : tactic 52 val ALL_LT : list_tactic 53 val TRY : tactic -> tactic 54 val TRY_LT : list_tactic -> list_tactic 55 val REPEAT : tactic -> tactic 56 val rpt : tactic -> tactic 57 val REPEAT_LT : list_tactic -> list_tactic 58 val VALID : tactic -> tactic 59 val VALID_LT : list_tactic -> list_tactic 60 val VALIDATE : tactic -> tactic 61 val VALIDATE_LT : list_tactic -> list_tactic 62 val GEN_VALIDATE : bool -> tactic -> tactic 63 val GEN_VALIDATE_LT: bool -> list_tactic -> list_tactic 64 val ADD_SGS_TAC : term list -> tactic -> tactic 65 val EVERY : tactic list -> tactic 66 val EVERY_LT : list_tactic list -> list_tactic 67 val FIRST : tactic list -> tactic 68 val MAP_EVERY : ('a -> tactic) -> 'a list -> tactic 69 val map_every : ('a -> tactic) -> 'a list -> tactic 70 val MAP_FIRST : ('a -> tactic) -> 'a list -> tactic 71 val FIRST_PROVE : tactic list -> tactic 72 val EVERY_ASSUM : thm_tactic -> tactic 73 val FIRST_ASSUM : thm_tactic -> tactic 74 val first_assum : thm_tactic -> tactic 75 val FIRST_X_ASSUM : thm_tactic -> tactic 76 val first_x_assum : thm_tactic -> tactic 77 val LAST_ASSUM : thm_tactic -> tactic 78 val last_assum : thm_tactic -> tactic 79 val LAST_X_ASSUM : thm_tactic -> tactic 80 val last_x_assum : thm_tactic -> tactic 81 val goal_assum : thm_tactic -> tactic 82 val hdtm_assum : term -> thm_tactic -> tactic 83 val hdtm_x_assum : term -> thm_tactic -> tactic 84 85 val ASSUM_LIST : (thm list -> tactic) -> tactic 86 val POP_ASSUM : thm_tactic -> tactic 87 val pop_assum : thm_tactic -> tactic 88 val PRED_ASSUM : (term -> bool) -> thm_tactic -> tactic 89 val PAT_ASSUM : term -> thm_tactic -> tactic 90 val PAT_X_ASSUM : term -> thm_tactic -> tactic 91 val POP_ASSUM_LIST : (thm list -> tactic) -> tactic 92 val SUBGOAL_THEN : term -> thm_tactic -> tactic 93 val USE_SG_THEN : thm_tactic -> int -> int -> list_tactic 94 val CHANGED_TAC : tactic -> tactic 95 val Q_TAC0 : {traces : (string * int) list} -> hol_type option -> 96 (term -> tactic) -> term quotation -> tactic 97 val Q_TAC : (term -> tactic) -> term quotation -> tactic 98 val QTY_TAC : hol_type -> (term -> tactic) -> term quotation -> tactic 99 100 val default_prover : term * tactic -> thm 101 val set_prover : (term * tactic -> thm) -> unit 102 val restore_prover : unit -> unit 103 104end 105