Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/thms.ML
author paulson
Thu, 31 May 2001 18:28:23 +0200
changeset 11354 9b80fe19407f
parent 10769 70b9b0cfe05f
child 11455 e07927b980ec
permissions -rw-r--r--
examples files start from Main instead of various ZF theories

(*  Title:      TFL/thms.ML
    ID:         $Id$
    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 "cut_def";
  val SELECT_AX = thm "tfl_some";
  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;
isabelle