1signature Thm_cont = 2sig 3 include Abbrev 4 5 val THEN_TCL : thm_tactical * thm_tactical -> thm_tactical 6 val ORELSE_TCL : thm_tactical * thm_tactical -> thm_tactical 7 val REPEAT_TCL : thm_tactical -> thm_tactical 8 val REPEAT_GTCL : thm_tactical -> (thm -> tactic) -> thm_tactic 9 val ALL_THEN : thm_tactical 10 val NO_THEN : thm_tactical 11 val EVERY_TCL : thm_tactical list -> thm_tactical 12 val FIRST_TCL : thm_tactical list -> thm_tactical 13 val CONJUNCTS_THEN2 : thm_tactic -> thm_tactical 14 val CONJUNCTS_THEN : thm_tactical 15 val DISJ_CASES_THEN2 : thm_tactic -> thm_tactical 16 val DISJ_CASES_THEN : thm_tactical 17 val DISJ_CASES_THENL : thm_tactic list -> thm_tactic 18 val DISCH_THEN : thm_tactic -> tactic 19 val disch_then : thm_tactic -> tactic 20 val UNDISCH_THEN : Term.term -> thm_tactic -> tactic 21 val X_CHOOSE_THEN : Term.term -> thm_tactical 22 val CHOOSE_THEN : thm_tactical 23 val X_CASES_THENL : (('a list -> 'b list -> ('a * 'b) list) 24 -> thm_tactic list -> (term list * thm_tactic) list) 25 -> thm_tactic list -> thm_tactic 26 val X_CASES_THEN : Term.term list list -> thm_tactical 27 val CASES_THENL : thm_tactic list -> thm_tactic 28 val STRIP_THM_THEN : thm_tactical 29 30 val ANTE_RES_THEN : thm_tactical 31 val IMP_RES_THEN : thm_tactic -> thm -> tactic 32 val RES_THEN : thm_tactic -> tactic 33 val PROVEHYP_THEN : (thm -> thm -> tactic) -> thm -> tactic 34 val provehyp_then : (thm -> thm -> tactic) -> thm -> tactic 35end 36