|
10769
|
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 SELECT_AX = thm "tfl_some";
|
|
|
13 |
val eqT = thm "tfl_eq_True";
|
|
|
14 |
val rev_eq_mp = thm "tfl_rev_eq_mp";
|
|
|
15 |
val simp_thm = thm "tfl_simp_thm";
|
|
|
16 |
val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
|
|
|
17 |
val imp_trans = thm "tfl_imp_trans";
|
|
|
18 |
val disj_assoc = thm "tfl_disj_assoc";
|
|
|
19 |
val tfl_disjE = thm "tfl_disjE";
|
|
|
20 |
val choose_thm = thm "tfl_exE";
|
|
|
21 |
end;
|