src/HOL/ex/Bubblesort.thy

--- a/src/HOL/ex/Bubblesort.thy	Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/Bubblesort.thy	Tue Oct 06 17:47:28 2015 +0200
@@ -1,12 +1,12 @@
 (* Author: Tobias Nipkow *)
 
-section {* Bubblesort *}
+section \<open>Bubblesort\<close>
 
 theory Bubblesort
 imports "~~/src/HOL/Library/Multiset"
 begin
 
-text{* This is \emph{a} version of bubblesort. *}
+text\<open>This is \emph{a} version of bubblesort.\<close>
 
 context linorder
 begin