axclass power moved to Nat.thy;
authorwenzelm
Fri, 10 Nov 2000 19:03:06 +0100
changeset 10433 6c5659d461dd
parent 10432 3dfbc913d184
child 10434 6ea4735c3955
axclass power moved to Nat.thy;
src/HOL/HOL.ML
src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL.ML	Fri Nov 10 19:02:37 2000 +0100
+++ b/src/HOL/HOL.ML	Fri Nov 10 19:03:06 2000 +0100
@@ -8,7 +8,6 @@
   val plusI = plusI;
   val minusI = minusI;
   val timesI = timesI;
-  val powerI = powerI;
   val eq_reflection = eq_reflection;
   val refl = refl;
   val subst = subst;
--- a/src/HOL/HOL_lemmas.ML	Fri Nov 10 19:02:37 2000 +0100
+++ b/src/HOL/HOL_lemmas.ML	Fri Nov 10 19:03:06 2000 +0100
@@ -11,7 +11,6 @@
 val plusI = thm "plusI";
 val minusI = thm "minusI";
 val timesI = thm "timesI";
-val powerI = thm "powerI";
 val eq_reflection = thm "eq_reflection";
 val refl = thm "refl";
 val subst = thm "subst";