equal
deleted
inserted
replaced
1070 |
1070 |
1071 |
1071 |
1072 subsection {* Word Arithmetic *} |
1072 subsection {* Word Arithmetic *} |
1073 |
1073 |
1074 lemma word_less_alt: "(a < b) = (uint a < uint b)" |
1074 lemma word_less_alt: "(a < b) = (uint a < uint b)" |
1075 unfolding word_less_def word_le_def |
1075 unfolding word_less_def word_le_def by (simp add: less_le) |
1076 by (auto simp del: word_uint.Rep_inject |
|
1077 simp: word_uint.Rep_inject [symmetric]) |
|
1078 |
1076 |
1079 lemma signed_linorder: "class.linorder word_sle word_sless" |
1077 lemma signed_linorder: "class.linorder word_sle word_sless" |
1080 proof |
1078 proof |
1081 qed (unfold word_sle_def word_sless_def, auto) |
1079 qed (unfold word_sle_def word_sless_def, auto) |
1082 |
1080 |