TFL/thms.sig
author paulson
Tue May 20 11:49:57 1997 +0200 (1997-05-20)
changeset 3245 241838c01caf
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
permissions -rw-r--r--
Removal of redundant code (unused or already present in Isabelle.
This eliminates HOL compatibility but makes the code smaller and more
readable
paulson@2112
     1
signature Thms_sig =
paulson@2112
     2
sig
paulson@3245
     3
   val WF_INDUCTION_THM:thm
paulson@3245
     4
   val WFREC_COROLLARY :thm
paulson@3245
     5
   val CUT_DEF         :thm
paulson@3245
     6
   val CUT_LEMMA       :thm
paulson@3245
     7
   val SELECT_AX       :thm
paulson@2112
     8
   
paulson@3245
     9
   val COND_CONG :thm
paulson@3245
    10
   val LET_CONG  :thm
paulson@2112
    11
paulson@3245
    12
   val eqT       :thm
paulson@3245
    13
   val rev_eq_mp :thm
paulson@3245
    14
   val simp_thm  :thm
paulson@2112
    15
end;