23150
|
1 |
(* Title: HOL/Tools/TFL/thms.ML
|
|
2 |
Author: Konrad Slind, Cambridge University Computer Laboratory
|
|
3 |
Copyright 1997 University of Cambridge
|
|
4 |
*)
|
|
5 |
|
|
6 |
structure Thms =
|
|
7 |
struct
|
39159
|
8 |
val WFREC_COROLLARY = @{thm tfl_wfrec};
|
|
9 |
val WF_INDUCTION_THM = @{thm tfl_wf_induct};
|
|
10 |
val CUT_DEF = @{thm cut_def};
|
|
11 |
val eqT = @{thm tfl_eq_True};
|
|
12 |
val rev_eq_mp = @{thm tfl_rev_eq_mp};
|
|
13 |
val simp_thm = @{thm tfl_simp_thm};
|
|
14 |
val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True};
|
|
15 |
val imp_trans = @{thm tfl_imp_trans};
|
|
16 |
val disj_assoc = @{thm tfl_disj_assoc};
|
|
17 |
val tfl_disjE = @{thm tfl_disjE};
|
|
18 |
val choose_thm = @{thm tfl_exE};
|
23150
|
19 |
end;
|