changeset 24368 | 4c2e80f30aeb |
parent 24350 | 4d74f37c6367 |
child 24384 | 0002537695df |
--- a/src/HOL/Word/Num_Lemmas.thy Mon Aug 20 23:00:17 2007 +0200 +++ b/src/HOL/Word/Num_Lemmas.thy Mon Aug 20 23:35:51 2007 +0200 @@ -26,9 +26,6 @@ apply auto done -lemma int_number_of: "number_of (y::int) = y" - by (simp add: number_of_eq) - lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto constdefs