src/HOL/HOL.ML
changeset 10433 6c5659d461dd
parent 10273 59570adf2d3c
child 11451 8abfb4f7bd02
equal deleted inserted replaced
10432:3dfbc913d184 10433:6c5659d461dd
     6 struct
     6 struct
     7   val thy = the_context ();
     7   val thy = the_context ();
     8   val plusI = plusI;
     8   val plusI = plusI;
     9   val minusI = minusI;
     9   val minusI = minusI;
    10   val timesI = timesI;
    10   val timesI = timesI;
    11   val powerI = powerI;
       
    12   val eq_reflection = eq_reflection;
    11   val eq_reflection = eq_reflection;
    13   val refl = refl;
    12   val refl = refl;
    14   val subst = subst;
    13   val subst = subst;
    15   val ext = ext;
    14   val ext = ext;
    16   val someI = someI;
    15   val someI = someI;