diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/Parallel.thy
--- a/src/HOL/Library/Parallel.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Parallel.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -1,12 +1,12 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-section {* Futures and parallel lists for code generated towards Isabelle/ML *}
+section \<open>Futures and parallel lists for code generated towards Isabelle/ML\<close>
 
 theory Parallel
 imports Main
 begin
 
-subsection {* Futures *}
+subsection \<open>Futures\<close>
 
 datatype 'a future = fork "unit \<Rightarrow> 'a"
 
@@ -26,7 +26,7 @@
 code_reserved Eval Future future
 
 
-subsection {* Parallel lists *}
+subsection \<open>Parallel lists\<close>
 
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
   [simp]: "map = List.map"