diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Bool_Discrete.thy
--- a/src/HOL/HOLCF/Library/Bool_Discrete.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Discrete cpo instance for booleans *}
+section \<open>Discrete cpo instance for booleans\<close>
 
 theory Bool_Discrete
 imports HOLCF
 begin
 
-text {* Discrete cpo instance for @{typ bool}. *}
+text \<open>Discrete cpo instance for @{typ bool}.\<close>
 
 instantiation bool :: discrete_cpo
 begin
@@ -21,9 +21,9 @@
 
 end
 
-text {*
+text \<open>
   TODO: implement a command to automate discrete predomain instances.
-*}
+\<close>
 
 instantiation bool :: predomain
 begin