TFL/thms.sig

Loop detection: before expanding a haz formula, see whether it is a duplicate
and, if so, delete it.

Recursion detection: transitivity and similar rules, when applied, put the
new formulae at the end of a branch and not at the front (in effect).

signature Thms_sig =
sig
   type Thm
   val WF_INDUCTION_THM:Thm
   val WFREC_COROLLARY :Thm
   val CUT_DEF         :Thm
   val CUT_LEMMA       :Thm
   val SELECT_AX       :Thm
   
   val COND_CONG :Thm
   val LET_CONG  :Thm

   val eqT       :Thm
   val rev_eq_mp :Thm
   val simp_thm  :Thm
end;