TFL/thms.ML
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 11455 e07927b980ec
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      TFL/thms.ML
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     5
*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     6
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     7
structure Thms =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     8
struct
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     9
  val WFREC_COROLLARY = thm "tfl_wfrec";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    10
  val WF_INDUCTION_THM = thm "tfl_wf_induct";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    11
  val CUT_DEF = thm "cut_def";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    12
  val eqT = thm "tfl_eq_True";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    13
  val rev_eq_mp = thm "tfl_rev_eq_mp";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    14
  val simp_thm = thm "tfl_simp_thm";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    15
  val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    16
  val imp_trans = thm "tfl_imp_trans";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    17
  val disj_assoc = thm "tfl_disj_assoc";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    18
  val tfl_disjE = thm "tfl_disjE";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    19
  val choose_thm = thm "tfl_exE";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    20
end;