src/HOL/HOL.ML
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18916 fda5b8dbbef6
child 20944 34b2c1bb7178
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
wenzelm@12999
     1
(* legacy ML bindings *)
wenzelm@11749
     2
berghofe@13638
     3
val choice_eq = thm "choice_eq";
wenzelm@12999
     4
wenzelm@12999
     5
structure HOL =
wenzelm@12999
     6
struct
wenzelm@12999
     7
  val eq_reflection = eq_reflection;
wenzelm@12999
     8
  val refl = refl;
wenzelm@12999
     9
  val subst = subst;
wenzelm@12999
    10
  val ext = ext;
wenzelm@12999
    11
  val impI = impI;
wenzelm@12999
    12
  val mp = mp;
wenzelm@12999
    13
  val True_def = True_def;
wenzelm@12999
    14
  val All_def = All_def;
wenzelm@12999
    15
  val Ex_def = Ex_def;
wenzelm@12999
    16
  val False_def = False_def;
wenzelm@12999
    17
  val not_def = not_def;
wenzelm@12999
    18
  val and_def = and_def;
wenzelm@12999
    19
  val or_def = or_def;
wenzelm@12999
    20
  val Ex1_def = Ex1_def;
wenzelm@12999
    21
  val iff = iff;
wenzelm@12999
    22
  val True_or_False = True_or_False;
wenzelm@12999
    23
  val Let_def = Let_def;
wenzelm@12999
    24
  val if_def = if_def;
wenzelm@12999
    25
end;
wenzelm@12999
    26
wenzelm@12999
    27
open HOL;
haftmann@18916
    28
haftmann@18916
    29
structure HOL =
haftmann@18916
    30
struct
haftmann@18916
    31
haftmann@18916
    32
open HOL;
haftmann@18916
    33
haftmann@18916
    34
val thy = the_context ();
haftmann@18916
    35
haftmann@18916
    36
end;