src/HOL/ex/Ballot.thy
changeset 70347 e5cd5471c18a
parent 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/ex/Ballot.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/ex/Ballot.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -223,13 +223,13 @@
     1.4  
     1.5        have "Suc a * (a - Suc b) + (Suc a - b) * Suc b =
     1.6          (Suc a * a - Suc a * Suc b) + (Suc a * Suc b - Suc b * b)"
     1.7 -        by (simp add: sign_simps)
     1.8 +        by (simp add: algebra_simps)
     1.9        also have "\<dots> = (Suc a * a + (Suc a * Suc b - Suc b * b)) - Suc a * Suc b"
    1.10          using \<open>b<a\<close> by (intro add_diff_assoc2 mult_mono) auto
    1.11        also have "\<dots> = (Suc a * a + Suc a * Suc b) - Suc b * b - Suc a * Suc b"
    1.12          using \<open>b<a\<close> by (intro arg_cong2[where f="(-)"] add_diff_assoc mult_mono) auto
    1.13        also have "\<dots> = (Suc a * Suc (a + b)) - (Suc b * Suc (a + b))"
    1.14 -        by (simp add: sign_simps)
    1.15 +        by (simp add: algebra_simps)
    1.16        finally have rearrange: "Suc a * (a - Suc b) + (Suc a - b) * Suc b = (Suc a - Suc b) * Suc (a + b)"
    1.17          unfolding diff_mult_distrib by simp
    1.18