thys/PositionsExt.thy
changeset 286 804fbb227568
parent 280 c840a99a3e05
--- 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)"