src/HOL/HOL.ML
author wenzelm
Thu Sep 27 16:04:11 2001 +0200 (2001-09-27)
changeset 11588 d792570a04b1
parent 11451 8abfb4f7bd02
child 11749 fc8afdc58b26
permissions -rw-r--r--
AddXEs [disjI1, disjI2];
     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 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   val arbitrary_def = arbitrary_def;
    30 end;
    31 
    32 AddXIs [equal_intr_rule, ext];
    33 AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
    34 
    35 open HOL;