equal
deleted
inserted
replaced
24 |
24 |
25 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)" |
25 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)" |
26 by simp |
26 by simp |
27 |
27 |
28 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)" |
28 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)" |
|
29 by simp |
|
30 |
|
31 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})" |
|
32 by simp |
|
33 |
|
34 lemma inverse_numeral_1: |
|
35 "inverse Numeral1 = (Numeral1::'a::{number_ring,field})" |
29 by simp |
36 by simp |
30 |
37 |
31 text{*Theorem lists for the cancellation simprocs. The use of binary numerals |
38 text{*Theorem lists for the cancellation simprocs. The use of binary numerals |
32 for 0 and 1 reduces the number of special cases.*} |
39 for 0 and 1 reduces the number of special cases.*} |
33 |
40 |