src/HOL/HOL.ML
author wenzelm
Tue Oct 10 23:43:23 2000 +0200 (2000-10-10)
changeset 10182 5413bcce1482
parent 10062 3b819da9c71a
child 10273 59570adf2d3c
permissions -rw-r--r--
AddXEs [someI_ex];
     1 (*  Title:      HOL/HOL.ML
     2     ID:         $Id$
     3 *)
     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 powerI = powerI;
    12   val eq_reflection = eq_reflection;
    13   val refl = refl;
    14   val subst = subst;
    15   val ext = ext;
    16   val someI = someI;
    17   val impI = impI;
    18   val mp = mp;
    19   val True_def = True_def;
    20   val All_def = All_def;
    21   val Ex_def = Ex_def;
    22   val False_def = False_def;
    23   val not_def = not_def;
    24   val and_def = and_def;
    25   val or_def = or_def;
    26   val Ex1_def = Ex1_def;
    27   val iff = iff;
    28   val True_or_False = True_or_False;
    29   val Let_def = Let_def;
    30   val if_def = if_def;
    31   val arbitrary_def = arbitrary_def;
    32 end;
    33 
    34 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
    35 AddXEs [ex1_implies_ex, someI_ex];
    36 
    37 open HOL;