src/HOL/HOL.ML
changeset 10433 6c5659d461dd
parent 10273 59570adf2d3c
child 11451 8abfb4f7bd02
     1.1 --- a/src/HOL/HOL.ML	Fri Nov 10 19:02:37 2000 +0100
     1.2 +++ b/src/HOL/HOL.ML	Fri Nov 10 19:03:06 2000 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4    val plusI = plusI;
     1.5    val minusI = minusI;
     1.6    val timesI = timesI;
     1.7 -  val powerI = powerI;
     1.8    val eq_reflection = eq_reflection;
     1.9    val refl = refl;
    1.10    val subst = subst;