src/HOL/Tools/TFL/thms.ML
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 23150 073a65f0bc40
child 58184 db1381d811ab
permissions -rw-r--r--
more antiquotations;
wenzelm@23150
     1
(*  Title:      HOL/Tools/TFL/thms.ML
wenzelm@23150
     2
    Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@23150
     3
    Copyright   1997  University of Cambridge
wenzelm@23150
     4
*)
wenzelm@23150
     5
wenzelm@23150
     6
structure Thms =
wenzelm@23150
     7
struct
wenzelm@39159
     8
  val WFREC_COROLLARY = @{thm tfl_wfrec};
wenzelm@39159
     9
  val WF_INDUCTION_THM = @{thm tfl_wf_induct};
wenzelm@39159
    10
  val CUT_DEF = @{thm cut_def};
wenzelm@39159
    11
  val eqT = @{thm tfl_eq_True};
wenzelm@39159
    12
  val rev_eq_mp = @{thm tfl_rev_eq_mp};
wenzelm@39159
    13
  val simp_thm = @{thm tfl_simp_thm};
wenzelm@39159
    14
  val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True};
wenzelm@39159
    15
  val imp_trans = @{thm tfl_imp_trans};
wenzelm@39159
    16
  val disj_assoc = @{thm tfl_disj_assoc};
wenzelm@39159
    17
  val tfl_disjE = @{thm tfl_disjE};
wenzelm@39159
    18
  val choose_thm = @{thm tfl_exE};
wenzelm@23150
    19
end;