src/HOL/Integ/NatBin.ML
changeset 9108 9fff97d29837
parent 9064 eacebbcafe57
child 9425 fd6866d90ec1
     1.1 --- a/src/HOL/Integ/NatBin.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -345,13 +345,13 @@
     1.4  Addsimps [inst "n" "number_of ?v" diff_less'];
     1.5  
     1.6  (*various theorems that aren't in the default simpset*)
     1.7 -val add_is_one' = rename_numerals thy add_is_1;
     1.8 -val one_is_add' = rename_numerals thy one_is_add;
     1.9 -val zero_induct' = rename_numerals thy zero_induct;
    1.10 -val diff_self_eq_0' = rename_numerals thy diff_self_eq_0;
    1.11 -val mult_eq_self_implies_10' = rename_numerals thy mult_eq_self_implies_10;
    1.12 -val le_pred_eq' = rename_numerals thy le_pred_eq;
    1.13 -val less_pred_eq' = rename_numerals thy less_pred_eq;
    1.14 +bind_thm ("add_is_one'", rename_numerals thy add_is_1);
    1.15 +bind_thm ("one_is_add'", rename_numerals thy one_is_add);
    1.16 +bind_thm ("zero_induct'", rename_numerals thy zero_induct);
    1.17 +bind_thm ("diff_self_eq_0'", rename_numerals thy diff_self_eq_0);
    1.18 +bind_thm ("mult_eq_self_implies_10'", rename_numerals thy mult_eq_self_implies_10);
    1.19 +bind_thm ("le_pred_eq'", rename_numerals thy le_pred_eq);
    1.20 +bind_thm ("less_pred_eq'", rename_numerals thy less_pred_eq);
    1.21  
    1.22  (** Divides **)
    1.23  
    1.24 @@ -361,10 +361,10 @@
    1.25  	  [dvd_1_left, dvd_0_right]);
    1.26  
    1.27  (*useful?*)
    1.28 -val mod_self' = rename_numerals thy mod_self;
    1.29 -val div_self' = rename_numerals thy div_self;
    1.30 -val div_less' = rename_numerals thy div_less;
    1.31 -val mod_mult_self_is_zero' = rename_numerals thy mod_mult_self_is_0;
    1.32 +bind_thm ("mod_self'", rename_numerals thy mod_self);
    1.33 +bind_thm ("div_self'", rename_numerals thy div_self);
    1.34 +bind_thm ("div_less'", rename_numerals thy div_less);
    1.35 +bind_thm ("mod_mult_self_is_zero'", rename_numerals thy mod_mult_self_is_0);
    1.36  
    1.37  (** Power **)
    1.38  
    1.39 @@ -386,9 +386,9 @@
    1.40  qed "zero_less_power'";
    1.41  Addsimps [zero_less_power'];
    1.42  
    1.43 -val binomial_zero = rename_numerals thy binomial_0;
    1.44 -val binomial_Suc' = rename_numerals thy binomial_Suc;
    1.45 -val binomial_n_n' = rename_numerals thy binomial_n_n;
    1.46 +bind_thm ("binomial_zero", rename_numerals thy binomial_0);
    1.47 +bind_thm ("binomial_Suc'", rename_numerals thy binomial_Suc);
    1.48 +bind_thm ("binomial_n_n'", rename_numerals thy binomial_n_n);
    1.49  
    1.50  (*binomial_0_Suc doesn't work well on numerals*)
    1.51  Addsimps (map (rename_numerals thy)