src/HOL/Int.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58512 dc4d76dfa8f0
```     1.1 --- a/src/HOL/Int.thy	Sat Jul 05 10:09:01 2014 +0200
1.2 +++ b/src/HOL/Int.thy	Sat Jul 05 11:01:53 2014 +0200
1.3 @@ -518,11 +518,11 @@
1.4
1.5  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
1.6    -- {* Unfold all @{text let}s involving constants *}
1.7 -  unfolding Let_def ..
1.8 +  by (fact Let_numeral) -- {* FIXME drop *}
1.9
1.10  lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
1.11    -- {* Unfold all @{text let}s involving constants *}
1.12 -  unfolding Let_def ..
1.13 +  by (fact Let_neg_numeral) -- {* FIXME drop *}
1.14
1.15  text {* Unfold @{text min} and @{text max} on numerals. *}
1.16
1.17 @@ -559,7 +559,7 @@
1.18  proof -
1.19    have "0 \<le> z" by fact
1.20    also have "... < z + 1" by (rule less_add_one)
1.21 -  also have "... = 1 + z" by (simp add: add_ac)
1.22 +  also have "... = 1 + z" by (simp add: ac_simps)
1.23    finally show "0 < 1 + z" .
1.24  qed
1.25
```