--- a/src/HOL/Analysis/Simplex_Content.thy Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Simplex_Content.thy Tue Mar 31 15:51:15 2020 +0200
@@ -252,7 +252,7 @@
((a + b + c) - 2 * c)"
unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps)
also have "\<dots> = 16 * s * (s - a) * (s - b) * (s - c)"
- by (simp add: s_def field_split_simps mult_ac)
+ by (simp add: s_def field_split_simps)
finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)"
by simp
also have "\<dots> = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2"