--- a/src/HOL/Power.thy Fri Mar 13 15:52:23 2009 +0100
+++ b/src/HOL/Power.thy Fri Mar 13 10:14:47 2009 -0700
@@ -412,56 +412,4 @@
by (induct m n rule: diff_induct)
(simp_all add: nonzero_mult_divide_cancel_left nz)
-
-text{*ML bindings for the general exponentiation theorems*}
-ML
-{*
-val power_0 = thm"power_0";
-val power_Suc = thm"power_Suc";
-val power_0_Suc = thm"power_0_Suc";
-val power_0_left = thm"power_0_left";
-val power_one = thm"power_one";
-val power_one_right = thm"power_one_right";
-val power_add = thm"power_add";
-val power_mult = thm"power_mult";
-val power_mult_distrib = thm"power_mult_distrib";
-val zero_less_power = thm"zero_less_power";
-val zero_le_power = thm"zero_le_power";
-val one_le_power = thm"one_le_power";
-val gt1_imp_ge0 = thm"gt1_imp_ge0";
-val power_gt1_lemma = thm"power_gt1_lemma";
-val power_gt1 = thm"power_gt1";
-val power_le_imp_le_exp = thm"power_le_imp_le_exp";
-val power_inject_exp = thm"power_inject_exp";
-val power_less_imp_less_exp = thm"power_less_imp_less_exp";
-val power_mono = thm"power_mono";
-val power_strict_mono = thm"power_strict_mono";
-val power_eq_0_iff = thm"power_eq_0_iff";
-val field_power_eq_0_iff = thm"power_eq_0_iff";
-val field_power_not_zero = thm"field_power_not_zero";
-val power_inverse = thm"power_inverse";
-val nonzero_power_divide = thm"nonzero_power_divide";
-val power_divide = thm"power_divide";
-val power_abs = thm"power_abs";
-val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";
-val zero_le_power_abs = thm "zero_le_power_abs";
-val power_minus = thm"power_minus";
-val power_Suc_less = thm"power_Suc_less";
-val power_strict_decreasing = thm"power_strict_decreasing";
-val power_decreasing = thm"power_decreasing";
-val power_Suc_less_one = thm"power_Suc_less_one";
-val power_increasing = thm"power_increasing";
-val power_strict_increasing = thm"power_strict_increasing";
-val power_le_imp_le_base = thm"power_le_imp_le_base";
-val power_inject_base = thm"power_inject_base";
-*}
-
-text{*ML bindings for the remaining theorems*}
-ML
-{*
-val nat_one_le_power = thm"nat_one_le_power";
-val nat_power_less_imp_less = thm"nat_power_less_imp_less";
-val nat_zero_less_power_iff = thm"nat_zero_less_power_iff";
-*}
-
end