equal
deleted
inserted
replaced
439 "neg (number_of (w BIT x)::'a) = |
439 "neg (number_of (w BIT x)::'a) = |
440 neg (number_of w :: 'a::{ordered_idom,number_ring})" |
440 neg (number_of w :: 'a::{ordered_idom,number_ring})" |
441 by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff |
441 by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff |
442 Ints_odd_less_0 Ints_def split: bit.split) |
442 Ints_odd_less_0 Ints_def split: bit.split) |
443 |
443 |
|
444 |
444 text {* Less-Than or Equals *} |
445 text {* Less-Than or Equals *} |
445 |
446 |
446 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} |
447 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} |
447 |
448 |
448 lemmas le_number_of_eq_not_less = |
449 lemmas le_number_of_eq_not_less = |