src/HOL/HOLCF/Plain_HOLCF.thy

--- a/src/HOL/HOLCF/Plain_HOLCF.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,15 +2,15 @@
     Author:     Brian Huffman
 *)
 
-section {* Plain HOLCF *}
+section \<open>Plain HOLCF\<close>
 
 theory Plain_HOLCF
 imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
 begin
 
-text {*
+text \<open>
   Basic HOLCF concepts and types; does not include definition packages.
-*}
+\<close>
 
 hide_const (open) Filter.principal