diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* A simple FIFO buffer (synchronous communication, interleaving) *}
+section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>
 
 theory Buffer
 imports "../TLA"