TFL/thms.sig
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3458 5ff4bfab859c
child 6498 1ebbe18fe236
permissions -rw-r--r--
tidying
     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;