equal
deleted
inserted
replaced
|
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; |