equal
deleted
inserted
replaced
105 |
105 |
106 definition [simp, code del]: |
106 definition [simp, code del]: |
107 "n < m \<longleftrightarrow> int_of n < int_of m" |
107 "n < m \<longleftrightarrow> int_of n < int_of m" |
108 |
108 |
109 instance proof |
109 instance proof |
110 qed (auto simp add: code_int left_distrib zmult_zless_mono2) |
110 qed (auto simp add: code_int distrib_right zmult_zless_mono2) |
111 |
111 |
112 end |
112 end |
113 |
113 |
114 lemma int_of_numeral [simp]: |
114 lemma int_of_numeral [simp]: |
115 "int_of (numeral k) = numeral k" |
115 "int_of (numeral k) = numeral k" |