src/HOL/Int.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58512 dc4d76dfa8f0
--- a/src/HOL/Int.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Int.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -518,11 +518,11 @@
 
 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. *}
 
@@ -559,7 +559,7 @@
 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