changeset 71938 | e1b262e7480c |
parent 69122 | 1b5178abaf97 |
--- a/src/HOL/Algebra/Cycles.thy Tue Jun 16 08:41:39 2020 +0000 +++ b/src/HOL/Algebra/Cycles.thy Tue Jun 16 08:41:39 2020 +0000 @@ -160,7 +160,7 @@ using aui_lemma[OF assms] by simp next case 2 thus ?thesis - using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps(8)) + using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps) next case 3 thus ?thesis by (simp add: id_outside_supp)