# HG changeset patch
# User haftmann
# Date 1614199509 -3600
# Node ID 47616dc81488df7d28c525a18f3f92d3345ac78b
# Parent  bfe92e4f6ea4c5883b8cd07e0292eb3e3b322c90
repaired document

diff -r bfe92e4f6ea4 -r 47616dc81488 src/HOL/Library/List_Permutation.thy
--- a/src/HOL/Library/List_Permutation.thy	Wed Feb 24 13:31:33 2021 +0000
+++ b/src/HOL/Library/List_Permutation.thy	Wed Feb 24 21:45:09 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>