TFL/thms.sig

Used nat_trans_tac. New Eta. various smaller changes.

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;