--- a/thys/Positions.thy Fri Feb 08 12:47:35 2019 +0000
+++ b/thys/Positions.thy Sun Feb 10 21:53:57 2019 +0000
@@ -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)"