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 eqT = thm "tfl_eq_True";


13 
val rev_eq_mp = thm "tfl_rev_eq_mp";


14 
val simp_thm = thm "tfl_simp_thm";


15 
val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";


16 
val imp_trans = thm "tfl_imp_trans";


17 
val disj_assoc = thm "tfl_disj_assoc";


18 
val tfl_disjE = thm "tfl_disjE";


19 
val choose_thm = thm "tfl_exE";


20 
end;
