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