src/HOL/HOL.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15524 2ef571f80a55
child 17274 746bb4c56800
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (* legacy ML bindings *)
     2 
     3 val choice_eq = thm "choice_eq";
     4 
     5 structure HOL =
     6 struct
     7   val thy = the_context ();
     8   val plusI = plusI;
     9   val minusI = minusI;
    10   val timesI = timesI;
    11   val eq_reflection = eq_reflection;
    12   val refl = refl;
    13   val subst = subst;
    14   val ext = ext;
    15   val impI = impI;
    16   val mp = mp;
    17   val True_def = True_def;
    18   val All_def = All_def;
    19   val Ex_def = Ex_def;
    20   val False_def = False_def;
    21   val not_def = not_def;
    22   val and_def = and_def;
    23   val or_def = or_def;
    24   val Ex1_def = Ex1_def;
    25   val iff = iff;
    26   val True_or_False = True_or_False;
    27   val Let_def = Let_def;
    28   val if_def = if_def;
    29 end;
    30 
    31 open HOL;