--- a/thys/PositionsExt.thy Wed May 16 20:58:39 2018 +0100
+++ b/thys/PositionsExt.thy Wed Aug 15 13:48:57 2018 +0100
@@ -126,7 +126,7 @@
-section {* POSIX Ordering of Values According to Okui & Suzuki *}
+section {* POSIX Ordering of Values According to Okui \& Suzuki *}
definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
@@ -196,9 +196,9 @@
using assms
using PosOrd_irrefl PosOrd_trans by blast
-text {*
+(*
:\<sqsubseteq>val and :\<sqsubset>val are partial orders.
-*}
+*)
lemma PosOrd_ordering:
shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"