TFL/thms.sig
changeset 3245 241838c01caf
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
equal deleted inserted replaced
3244:71b760618f30 3245:241838c01caf
     1 signature Thms_sig =
     1 signature Thms_sig =
     2 sig
     2 sig
     3    type Thm
     3    val WF_INDUCTION_THM:thm
     4    val WF_INDUCTION_THM:Thm
     4    val WFREC_COROLLARY :thm
     5    val WFREC_COROLLARY :Thm
     5    val CUT_DEF         :thm
     6    val CUT_DEF         :Thm
     6    val CUT_LEMMA       :thm
     7    val CUT_LEMMA       :Thm
     7    val SELECT_AX       :thm
     8    val SELECT_AX       :Thm
       
     9    
     8    
    10    val COND_CONG :Thm
     9    val COND_CONG :thm
    11    val LET_CONG  :Thm
    10    val LET_CONG  :thm
    12 
    11 
    13    val eqT       :Thm
    12    val eqT       :thm
    14    val rev_eq_mp :Thm
    13    val rev_eq_mp :thm
    15    val simp_thm  :Thm
    14    val simp_thm  :thm
    16 end;
    15 end;