diff -r db6bedfba498 -r 3950e65f48f8 src/HOL/Integ/Numeral.thy --- 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\b"} to @{term "~ (b