src/HOL/HOL.ML
author paulson
Fri Sep 15 15:30:50 2000 +0200 (2000-09-15)
changeset 9970 dfe4747c8318
parent 9396 a1b31d61f8e1
child 10011 ed5262aee27f
permissions -rw-r--r--
the final renaming: selectI -> someI
     1 structure HOL =
     2 struct
     3   val thy = the_context ();
     4   val plusI = plusI;
     5   val minusI = minusI;
     6   val timesI = timesI;
     7   val powerI = powerI;
     8   val eq_reflection = eq_reflection;
     9   val refl = refl;
    10   val subst = subst;
    11   val ext = ext;
    12   val someI = someI;
    13   val impI = impI;
    14   val mp = mp;
    15   val True_def = True_def;
    16   val All_def = All_def;
    17   val Ex_def = Ex_def;
    18   val False_def = False_def;
    19   val not_def = not_def;
    20   val and_def = and_def;
    21   val or_def = or_def;
    22   val Ex1_def = Ex1_def;
    23   val iff = iff;
    24   val True_or_False = True_or_False;
    25   val Let_def = Let_def;
    26   val if_def = if_def;
    27   val arbitrary_def = arbitrary_def;
    28 end;
    29 
    30 AddXIs [disjI1, disjI2];
    31 
    32 open HOL;