diff -r 060efe532189 -r 64d928bacddd src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Fri Jan 12 17:14:34 2018 +0100
+++ b/src/HOL/Hoare/Separation.thy	Fri Jan 12 17:58:03 2018 +0100
@@ -156,7 +156,7 @@
 proofs. Here comes a simple example of a program proof that uses a law
 of separation logic instead.\<close>
 
-(* a law of separation logic *)
+\<comment> \<open>a law of separation logic\<close>
 lemma star_comm: "P ** Q = Q ** P"
   by(auto simp add:star_def ortho_def dest: map_add_comm)