remove legacy ML bindings
authorhuffman
Fri Mar 13 10:14:47 2009 -0700 (2009-03-13)
changeset 3051668b4a06cbd5c
parent 30507 20a95d8dd7c8
child 30520 c4728771f04f
remove legacy ML bindings
src/HOL/Power.thy
     1.1 --- a/src/HOL/Power.thy	Fri Mar 13 15:52:23 2009 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Mar 13 10:14:47 2009 -0700
     1.3 @@ -412,56 +412,4 @@
     1.4    by (induct m n rule: diff_induct)
     1.5      (simp_all add: nonzero_mult_divide_cancel_left nz)
     1.6  
     1.7 -
     1.8 -text{*ML bindings for the general exponentiation theorems*}
     1.9 -ML
    1.10 -{*
    1.11 -val power_0 = thm"power_0";
    1.12 -val power_Suc = thm"power_Suc";
    1.13 -val power_0_Suc = thm"power_0_Suc";
    1.14 -val power_0_left = thm"power_0_left";
    1.15 -val power_one = thm"power_one";
    1.16 -val power_one_right = thm"power_one_right";
    1.17 -val power_add = thm"power_add";
    1.18 -val power_mult = thm"power_mult";
    1.19 -val power_mult_distrib = thm"power_mult_distrib";
    1.20 -val zero_less_power = thm"zero_less_power";
    1.21 -val zero_le_power = thm"zero_le_power";
    1.22 -val one_le_power = thm"one_le_power";
    1.23 -val gt1_imp_ge0 = thm"gt1_imp_ge0";
    1.24 -val power_gt1_lemma = thm"power_gt1_lemma";
    1.25 -val power_gt1 = thm"power_gt1";
    1.26 -val power_le_imp_le_exp = thm"power_le_imp_le_exp";
    1.27 -val power_inject_exp = thm"power_inject_exp";
    1.28 -val power_less_imp_less_exp = thm"power_less_imp_less_exp";
    1.29 -val power_mono = thm"power_mono";
    1.30 -val power_strict_mono = thm"power_strict_mono";
    1.31 -val power_eq_0_iff = thm"power_eq_0_iff";
    1.32 -val field_power_eq_0_iff = thm"power_eq_0_iff";
    1.33 -val field_power_not_zero = thm"field_power_not_zero";
    1.34 -val power_inverse = thm"power_inverse";
    1.35 -val nonzero_power_divide = thm"nonzero_power_divide";
    1.36 -val power_divide = thm"power_divide";
    1.37 -val power_abs = thm"power_abs";
    1.38 -val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";
    1.39 -val zero_le_power_abs = thm "zero_le_power_abs";
    1.40 -val power_minus = thm"power_minus";
    1.41 -val power_Suc_less = thm"power_Suc_less";
    1.42 -val power_strict_decreasing = thm"power_strict_decreasing";
    1.43 -val power_decreasing = thm"power_decreasing";
    1.44 -val power_Suc_less_one = thm"power_Suc_less_one";
    1.45 -val power_increasing = thm"power_increasing";
    1.46 -val power_strict_increasing = thm"power_strict_increasing";
    1.47 -val power_le_imp_le_base = thm"power_le_imp_le_base";
    1.48 -val power_inject_base = thm"power_inject_base";
    1.49 -*}
    1.50 -
    1.51 -text{*ML bindings for the remaining theorems*}
    1.52 -ML
    1.53 -{*
    1.54 -val nat_one_le_power = thm"nat_one_le_power";
    1.55 -val nat_power_less_imp_less = thm"nat_power_less_imp_less";
    1.56 -val nat_zero_less_power_iff = thm"nat_zero_less_power_iff";
    1.57 -*}
    1.58 -
    1.59  end