equal
deleted
inserted
replaced
692 diff_nat_number_of |
692 diff_nat_number_of |
693 mult_nat_number_of |
693 mult_nat_number_of |
694 eq_nat_number_of |
694 eq_nat_number_of |
695 less_nat_number_of |
695 less_nat_number_of |
696 |
696 |
|
697 lemmas semiring_norm = |
|
698 Let_def arith_simps nat_arith rel_simps neg_simps if_False |
|
699 if_True add_0 add_Suc add_number_of_left mult_number_of_left |
|
700 numeral_1_eq_1 [symmetric] Suc_eq_plus1 |
|
701 numeral_0_eq_0 [symmetric] numerals [symmetric] |
|
702 iszero_simps not_iszero_Numeral1 |
|
703 |
697 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" |
704 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" |
698 by (fact Let_def) |
705 by (fact Let_def) |
699 |
706 |
700 lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})" |
707 lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})" |
701 by (simp only: number_of_Min power_minus1_even) |
708 by (simp only: number_of_Min power_minus1_even) |