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