| changeset 20596 | 3950e65f48f8 |
| parent 20500 | 11da1ce8dbd8 |
| child 20699 | 0cc77abb185a |
--- a/src/HOL/Integ/Numeral.thy Tue Sep 19 15:21:58 2006 +0200 +++ b/src/HOL/Integ/Numeral.thy Tue Sep 19 15:22:03 2006 +0200 @@ -441,6 +441,7 @@ by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff Ints_odd_less_0 Ints_def split: bit.split) + text {* Less-Than or Equals *} text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}