diff -r a730a5a0bab9 -r 89e6605c4ca4 thys/Positions.thy
--- a/thys/Positions.thy	Tue Jul 23 21:21:49 2019 +0100
+++ b/thys/Positions.thy	Mon Jul 29 09:37:20 2019 +0100
@@ -3,9 +3,9 @@
   imports "Spec" "Lexer"
 begin
 
-chapter {* An alternative definition for POSIX values *}
+chapter \<open>An alternative definition for POSIX values\<close>
 
-section {* Positions in Values *}
+section \<open>Positions in Values\<close>
 
 fun 
   at :: "val \<Rightarrow> nat list \<Rightarrow> val"
@@ -76,7 +76,7 @@
 
 
 
-section {* Orderings *}
+section \<open>Orderings\<close>
 
 
 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
@@ -128,7 +128,7 @@
 
 
 
-section {* POSIX Ordering of Values According to Okui \& Suzuki *}
+section \<open>POSIX Ordering of Values According to Okui \& Suzuki\<close>
 
 
 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
@@ -512,7 +512,7 @@
 
 
 
-section {* The Posix Value is smaller than any other Value *}
+section \<open>The Posix Value is smaller than any other Value\<close>
 
 
 lemma Posix_PosOrd: