--- a/src/HOL/Divides.thy Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/Divides.thy Wed Jun 11 14:24:23 2014 +1000
@@ -461,7 +461,7 @@
apply (case_tac "y = 0") apply simp
apply (auto simp add: dvd_def)
apply (subgoal_tac "-(y * k) = y * - k")
- apply (erule ssubst)
+ apply (simp only:)
apply (erule div_mult_self1_is_id)
apply simp
done
@@ -470,8 +470,7 @@
apply (case_tac "y = 0") apply simp
apply (auto simp add: dvd_def)
apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst)
- apply (rule div_mult_self1_is_id)
+ apply (erule ssubst, rule div_mult_self1_is_id)
apply simp
apply simp
done