(* 便利な推論規則とタクティック *)


val R_TAC = REWRITE_TAC;;

fun EQ_SYM_RULE th = ONCE_REWRITE_RULE [EQ_SYM_EQ] th;;

fun LET_RULE th = CONV_RULE (DEPTH_CONV let_CONV) th;;

val LET_TAC = CONV_TAC (DEPTH_CONV let_CONV) THEN REWRITE_TAC [];;

val LETR_TAC = LET_TAC;;


fun THM_UNDISCH_TAC thm = UNDISCH_TAC (#2(dest_thm(thm)));;

val UNDISCH_ALL_TAC = 
    REPEAT (ASSUM_LIST (fn thl => THM_UNDISCH_TAC (Lib.el 1 thl)));;


fun string_to_term s = Term [QUOTE s];;

fun PAIR_TAC t =
    let
	val s1 = term_to_string t
	val s2 = s1 ^ " = (FST (" ^ s1 ^ "),SND (" ^ s1 ^ "))"
	val lemma = prove(string_to_term s2, REWRITE_TAC [])
    in
	PURE_ONCE_REWRITE_TAC [lemma]
    end;;


fun ID_NO tac (l,t) =
    let
	val (l1,x) = tac (l,t)
    in
	if l1=[] then (l1,x)
	else if hd l1 = (l,t) then NO_TAC (l,t) 
	     else (l1,x)
    end;;