src/HOL/Int.thy

   assumes "0 \<le> k" obtains n where "k = int n"
   using assms by (rule nonneg_eq_int)
 
 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
-  unfolding Let_def ..
+  by (fact Let_numeral) -- {* FIXME drop *}
 
 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
-  unfolding Let_def ..
+  by (fact Let_neg_numeral) -- {* FIXME drop *}
 
 text {* Unfold @{text min} and @{text max} on numerals. *}
 
 lemmas max_number_of [simp] =
   max_def [of "numeral u" "numeral v"]

   assumes le: "0 \<le> z"
   shows "(0::int) < 1 + z"
 proof -
   have "0 \<le> z" by fact
   also have "... < z + 1" by (rule less_add_one)
-  also have "... = 1 + z" by (simp add: add_ac)
+  also have "... = 1 + z" by (simp add: ac_simps)
   finally show "0 < 1 + z" .
 qed
 
 lemma odd_less_0_iff:
   "(1 + z + z < 0) = (z < (0::int))"