--- a/src/HOL/Library/List_Permutation.thy Wed Feb 24 18:41:39 2021 +0000
+++ b/src/HOL/Library/List_Permutation.thy Thu Feb 25 13:35:54 2021 +0100
@@ -8,7 +8,7 @@
imports Multiset
begin
-subsection \<open>An inductive definition\<dots>\<close>
+subsection \<open>An inductive definition \ldots\<close>
inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50)
where
@@ -20,7 +20,7 @@
proposition perm_refl [iff]: "l <~~> l"
by (induct l) auto
-text \<open>\<dots>that is equivalent to an already existing notion:\<close>
+text \<open>\ldots that is equivalent to an already existing notion:\<close>
lemma perm_iff_eq_mset:
\<open>xs <~~> ys \<longleftrightarrow> mset xs = mset ys\<close>