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
     1 (* legacy ML bindings *)
     2 
     3 val choice_eq = thm "choice_eq";
     4 
     5 structure HOL =
     6 struct
     7   val eq_reflection = eq_reflection;
     8   val refl = refl;
     9   val subst = subst;
    10   val ext = ext;
    11   val impI = impI;
    12   val mp = mp;
    13   val True_def = True_def;
    14   val All_def = All_def;
    15   val Ex_def = Ex_def;
    16   val False_def = False_def;
    17   val not_def = not_def;
    18   val and_def = and_def;
    19   val or_def = or_def;
    20   val Ex1_def = Ex1_def;
    21   val iff = iff;
    22   val True_or_False = True_or_False;
    23   val Let_def = Let_def;
    24   val if_def = if_def;
    25 end;
    26 
    27 open HOL;
    28 
    29 structure HOL =
    30 struct
    31 
    32 open HOL;
    33 
    34 val thy = the_context ();
    35 
    36 end;