src/HOL/HOL.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7529 fa534e4f7e49
child 9396 a1b31d61f8e1
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 
     2 structure HOL =
     3 struct
     4   val thy = the_context ();
     5   val plusI = plusI;
     6   val minusI = minusI;
     7   val timesI = timesI;
     8   val powerI = powerI;
     9   val eq_reflection = eq_reflection;
    10   val refl = refl;
    11   val subst = subst;
    12   val ext = ext;
    13   val selectI = selectI;
    14   val impI = impI;
    15   val mp = mp;
    16   val True_def = True_def;
    17   val All_def = All_def;
    18   val Ex_def = Ex_def;
    19   val False_def = False_def;
    20   val not_def = not_def;
    21   val and_def = and_def;
    22   val or_def = or_def;
    23   val Ex1_def = Ex1_def;
    24   val iff = iff;
    25   val True_or_False = True_or_False;
    26   val Let_def = Let_def;
    27   val if_def = if_def;
    28   val arbitrary_def = arbitrary_def;
    29 end;
    30 
    31 AddXIs [disjI1, disjI2];
    32 
    33 open HOL;