src/HOL/HOL.ML
changeset 10062 3b819da9c71a
parent 10011 ed5262aee27f
child 10182 5413bcce1482
equal deleted inserted replaced
10061:fe82134773dc 10062:3b819da9c71a
    29   val Let_def = Let_def;
    29   val Let_def = Let_def;
    30   val if_def = if_def;
    30   val if_def = if_def;
    31   val arbitrary_def = arbitrary_def;
    31   val arbitrary_def = arbitrary_def;
    32 end;
    32 end;
    33 
    33 
    34 AddXIs [disjI1, disjI2, ext];
    34 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
       
    35 AddXEs [ex1_implies_ex];
    35 
    36 
    36 open HOL;
    37 open HOL;