TFL/thms.sig
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
signature Thms_sig =
paulson@2112
     2
sig
paulson@2112
     3
   type Thm
paulson@2112
     4
   val WF_INDUCTION_THM:Thm
paulson@2112
     5
   val WFREC_COROLLARY :Thm
paulson@2112
     6
   val CUT_DEF         :Thm
paulson@2112
     7
   val CUT_LEMMA       :Thm
paulson@2112
     8
   val SELECT_AX       :Thm
paulson@2112
     9
   
paulson@2112
    10
   val COND_CONG :Thm
paulson@2112
    11
   val LET_CONG  :Thm
paulson@2112
    12
paulson@2112
    13
   val eqT       :Thm
paulson@2112
    14
   val rev_eq_mp :Thm
paulson@2112
    15
   val simp_thm  :Thm
paulson@2112
    16
end;