TFL/thms.ML
author nipkow
Wed May 26 14:57:06 2004 +0200 (2004-05-26)
changeset 14804 8de39d3e8eb6
parent 11455 e07927b980ec
permissions -rw-r--r--
Corrected printer bug for bounded quantifiers Q x<=y. P
     1 (*  Title:      TFL/thms.ML
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 structure Thms =
     8 struct
     9   val WFREC_COROLLARY = thm "tfl_wfrec";
    10   val WF_INDUCTION_THM = thm "tfl_wf_induct";
    11   val CUT_DEF = thm "cut_def";
    12   val eqT = thm "tfl_eq_True";
    13   val rev_eq_mp = thm "tfl_rev_eq_mp";
    14   val simp_thm = thm "tfl_simp_thm";
    15   val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
    16   val imp_trans = thm "tfl_imp_trans";
    17   val disj_assoc = thm "tfl_disj_assoc";
    18   val tfl_disjE = thm "tfl_disjE";
    19   val choose_thm = thm "tfl_exE";
    20 end;