TFL/thms.sig
author paulson
Fri, 18 Oct 1996 12:41:04 +0200
changeset 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
Konrad Slind's TFL

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;