thys/Positions.thy
changeset 307 ee1caac29bb2
parent 292 d688a01b8f89
child 311 8b8db9558ecf
--- 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)"