src/HOL/HOL.ML
author wenzelm
Fri Nov 10 19:03:06 2000 +0100 (2000-11-10)
changeset 10433 6c5659d461dd
parent 10273 59570adf2d3c
child 11451 8abfb4f7bd02
permissions -rw-r--r--
axclass power moved to Nat.thy;
     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 someI = someI;
    16   val impI = impI;
    17   val mp = mp;
    18   val True_def = True_def;
    19   val All_def = All_def;
    20   val Ex_def = Ex_def;
    21   val False_def = False_def;
    22   val not_def = not_def;
    23   val and_def = and_def;
    24   val or_def = or_def;
    25   val Ex1_def = Ex1_def;
    26   val iff = iff;
    27   val True_or_False = True_or_False;
    28   val Let_def = Let_def;
    29   val if_def = if_def;
    30   val arbitrary_def = arbitrary_def;
    31 end;
    32 
    33 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
    34 AddXEs [ex1_implies_ex, someI_ex, sym];
    35 
    36 open HOL;