src/HOL/HOL.ML
author wenzelm
Thu Oct 19 21:20:53 2000 +0200 (2000-10-19)
changeset 10273 59570adf2d3c
parent 10182 5413bcce1482
child 10433 6c5659d461dd
permissions -rw-r--r--
declare sym [elim?] in HOL.ML instead of Calculation.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 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, sym];
    36 
    37 open HOL;