src/HOL/HOL.ML
changeset 9970 dfe4747c8318
parent 9396 a1b31d61f8e1
child 10011 ed5262aee27f
equal deleted inserted replaced
9969:4753185f1dd2 9970:dfe4747c8318
     7   val powerI = powerI;
     7   val powerI = powerI;
     8   val eq_reflection = eq_reflection;
     8   val eq_reflection = eq_reflection;
     9   val refl = refl;
     9   val refl = refl;
    10   val subst = subst;
    10   val subst = subst;
    11   val ext = ext;
    11   val ext = ext;
    12   val selectI = selectI;
    12   val someI = someI;
    13   val impI = impI;
    13   val impI = impI;
    14   val mp = mp;
    14   val mp = mp;
    15   val True_def = True_def;
    15   val True_def = True_def;
    16   val All_def = All_def;
    16   val All_def = All_def;
    17   val Ex_def = Ex_def;
    17   val Ex_def = Ex_def;