TFL/thms.sig
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 3458 5ff4bfab859c
child 6498 1ebbe18fe236
permissions -rw-r--r--
adapted extend_trfunsT;
     1 (*  Title:      TFL/thms
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 signature Thms_sig =
     8 sig
     9    val WF_INDUCTION_THM:thm
    10    val WFREC_COROLLARY :thm
    11    val CUT_DEF         :thm
    12    val CUT_LEMMA       :thm
    13    val SELECT_AX       :thm
    14    
    15    val LET_CONG  :thm
    16 
    17    val eqT       :thm
    18    val rev_eq_mp :thm
    19    val simp_thm  :thm
    20 end;