(* Title: HOL/Tools/TFL/thms.ML
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
*)
structure Thms =
struct
val WFREC_COROLLARY = @{thm tfl_wfrec};
val WF_INDUCTION_THM = @{thm tfl_wf_induct};
val CUT_DEF = @{thm tfl_cut_def};
val eqT = @{thm tfl_eq_True};
val rev_eq_mp = @{thm tfl_rev_eq_mp};
val simp_thm = @{thm tfl_simp_thm};
val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True};
val imp_trans = @{thm tfl_imp_trans};
val disj_assoc = @{thm tfl_disj_assoc};
val tfl_disjE = @{thm tfl_disjE};
val choose_thm = @{thm tfl_exE};
end;