diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Library/Sublist.thy --- 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 \Parallel lists\ -definition parallel :: "'a list \ 'a list \ bool" (infixl "\" 50) +definition parallel :: "'a list \ 'a list \ bool" (infixl \\\ 50) where "(xs \ ys) = (\ prefix xs ys \ \ prefix ys xs)" lemma parallelI [intro]: "\ prefix xs ys \ \ prefix ys xs \ xs \ ys"