1.1 --- a/src/HOL/Integ/Presburger.thy Tue May 11 14:00:02 2004 +0200
1.2 +++ b/src/HOL/Integ/Presburger.thy Tue May 11 20:11:08 2004 +0200
1.3 @@ -704,7 +704,7 @@
1.4 have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
1.5 also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
1.6 using minus[THEN spec, of "x - i * d"]
1.7 - by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric])
1.8 + by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
1.9 ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
1.10 qed
1.11 qed