author | wenzelm |
Wed, 17 Jun 2015 17:54:09 +0200 | |
changeset 60502 | aa58872267ee |
parent 58184 | db1381d811ab |
permissions | -rw-r--r-- |
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}; |
|
58184
db1381d811ab
cleanup Wfrec; introduce dependent_wf/wellorder_choice
hoelzl
parents:
39159
diff
changeset
|
10 |
val CUT_DEF = @{thm tfl_cut_def}; |
39159 | 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; |