TFL/thms.ML
author paulson
Wed Jul 25 13:13:01 2001 +0200 (2001-07-25)
changeset 11451 8abfb4f7bd02
parent 10769 70b9b0cfe05f
child 11455 e07927b980ec
permissions -rw-r--r--
partial restructuring to reduce dependence on Axiom of Choice
wenzelm@10769
     1
(*  Title:      TFL/thms.ML
wenzelm@10769
     2
    ID:         $Id$
wenzelm@10769
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@10769
     4
    Copyright   1997  University of Cambridge
wenzelm@10769
     5
*)
wenzelm@10769
     6
wenzelm@10769
     7
structure Thms =
wenzelm@10769
     8
struct
wenzelm@10769
     9
  val WFREC_COROLLARY = thm "tfl_wfrec";
wenzelm@10769
    10
  val WF_INDUCTION_THM = thm "tfl_wf_induct";
wenzelm@10769
    11
  val CUT_DEF = thm "cut_def";
wenzelm@10769
    12
  val SELECT_AX = thm "tfl_some";
wenzelm@10769
    13
  val eqT = thm "tfl_eq_True";
wenzelm@10769
    14
  val rev_eq_mp = thm "tfl_rev_eq_mp";
wenzelm@10769
    15
  val simp_thm = thm "tfl_simp_thm";
wenzelm@10769
    16
  val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
wenzelm@10769
    17
  val imp_trans = thm "tfl_imp_trans";
wenzelm@10769
    18
  val disj_assoc = thm "tfl_disj_assoc";
wenzelm@10769
    19
  val tfl_disjE = thm "tfl_disjE";
wenzelm@10769
    20
  val choose_thm = thm "tfl_exE";
wenzelm@10769
    21
end;