--- a/src/HOL/Library/Sublist.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Sublist.thy Fri Sep 20 19:51:08 2024 +0200
@@ -473,7 +473,7 @@
subsection \<open>Parallel lists\<close>
-definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<parallel>" 50)
+definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl \<open>\<parallel>\<close> 50)
where "(xs \<parallel> ys) = (\<not> prefix xs ys \<and> \<not> prefix ys xs)"
lemma parallelI [intro]: "\<not> prefix xs ys \<Longrightarrow> \<not> prefix ys xs \<Longrightarrow> xs \<parallel> ys"