src/HOL/Tools/TFL/thms.ML
author hoelzl
Thu Sep 04 14:02:37 2014 +0200 (2014-09-04)
changeset 58184 db1381d811ab
parent 39159 0dec18004e75
permissions -rw-r--r--
cleanup Wfrec; introduce dependent_wf/wellorder_choice
     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
     8   val WFREC_COROLLARY = @{thm tfl_wfrec};
     9   val WF_INDUCTION_THM = @{thm tfl_wf_induct};
    10   val CUT_DEF = @{thm tfl_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};
    19 end;