diff -r 6756b026c5fe -r ee1caac29bb2 thys/Positions.thy --- 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 \ nat list \ val \ bool" ("_ \val _ _" [60, 60, 59] 60) @@ -196,9 +196,9 @@ using assms using PosOrd_irrefl PosOrd_trans by blast -text {* +(* :\val and :\val are partial orders. -*} +*) lemma PosOrd_ordering: shows "ordering (\v1 v2. v1 :\val v2) (\ v1 v2. v1 :\val v2)"