# HG changeset patch
# User wenzelm
# Date 973879386 -3600
# Node ID 6c5659d461dd9872c434c99bd7fee99bb63316eb
# Parent  3dfbc913d1842ccc1dcdfac34c0abcd154d3f299
axclass power moved to Nat.thy;

diff -r 3dfbc913d184 -r 6c5659d461dd src/HOL/HOL.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;
diff -r 3dfbc913d184 -r 6c5659d461dd src/HOL/HOL_lemmas.ML
--- 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";