--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Sat Aug 12 10:09:29 2023 +0100
@@ -437,7 +437,7 @@
then obtain L where L: "subspace L" "affine_parallel S L"
using assms affine_parallel_subspace[of S] by auto
then obtain a where a: "S = ((+) a ` L)"
- using affine_parallel_def[of L S] affine_parallel_commut by auto
+ using affine_parallel_def[of L S] affine_parallel_commute by auto
from L have "closed L" using closed_subspace by auto
then have "closed S"
using closed_translation a by auto