src/HOL/Presburger.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58777 6ba2f1fa243b
     1.1 --- a/src/HOL/Presburger.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4  proof
     1.5    assume ?LHS
     1.6    then obtain x where P: "P x" ..
     1.7 -  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
     1.8 +  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality ac_simps eq_diff_eq)
     1.9    hence Pmod: "P x = P(x mod d)" using modd by simp
    1.10    show ?RHS
    1.11    proof (cases)
    1.12 @@ -307,7 +307,7 @@
    1.13    {fix x
    1.14      have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
    1.15      also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
    1.16 -      by (simp add:int_distrib add_ac)
    1.17 +      by (simp add:int_distrib ac_simps)
    1.18      ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
    1.19    thus ?case ..
    1.20  qed