src/HOL/HOL.ML
changeset 10011 ed5262aee27f
parent 9970 dfe4747c8318
child 10062 3b819da9c71a
equal deleted inserted replaced
10010:f6ccb6df9cb9 10011:ed5262aee27f
       
     1 (*  Title:      HOL/HOL.ML
       
     2     ID:         $Id$
       
     3 *)
       
     4 
     1 structure HOL =
     5 structure HOL =
     2 struct
     6 struct
     3   val thy = the_context ();
     7   val thy = the_context ();
     4   val plusI = plusI;
     8   val plusI = plusI;
     5   val minusI = minusI;
     9   val minusI = minusI;
    25   val Let_def = Let_def;
    29   val Let_def = Let_def;
    26   val if_def = if_def;
    30   val if_def = if_def;
    27   val arbitrary_def = arbitrary_def;
    31   val arbitrary_def = arbitrary_def;
    28 end;
    32 end;
    29 
    33 
    30 AddXIs [disjI1, disjI2];
    34 AddXIs [disjI1, disjI2, ext];
    31 
    35 
    32 open HOL;
    36 open HOL;