src/HOL/HOL.ML
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 18916 fda5b8dbbef6
child 20944 34b2c1bb7178
permissions -rw-r--r--
simplified code generator setup
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;