TFL/thms.sig
changeset 3458 5ff4bfab859c
parent 3302 404fe31fd8d2
child 6498 1ebbe18fe236
equal deleted inserted replaced
3457:a8ab7c64817c 3458:5ff4bfab859c
    10    val WFREC_COROLLARY :thm
    10    val WFREC_COROLLARY :thm
    11    val CUT_DEF         :thm
    11    val CUT_DEF         :thm
    12    val CUT_LEMMA       :thm
    12    val CUT_LEMMA       :thm
    13    val SELECT_AX       :thm
    13    val SELECT_AX       :thm
    14    
    14    
    15    val COND_CONG :thm
       
    16    val LET_CONG  :thm
    15    val LET_CONG  :thm
    17 
    16 
    18    val eqT       :thm
    17    val eqT       :thm
    19    val rev_eq_mp :thm
    18    val rev_eq_mp :thm
    20    val simp_thm  :thm
    19    val simp_thm  :thm