src/HOL/Presburger.thy
changeset 44766 d4d33a4d7548
parent 36804 f4ad04780669
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Presburger.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Presburger.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -308,7 +308,7 @@
     1.4    {fix x
     1.5      have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
     1.6      also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
     1.7 -      by (simp add:int_distrib zadd_ac)
     1.8 +      by (simp add:int_distrib add_ac)
     1.9      ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
    1.10    thus ?case ..
    1.11  qed