diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/SPARK/SPARK.thy
--- a/src/HOL/SPARK/SPARK.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/SPARK/SPARK.thy	Thu May 26 17:51:22 2016 +0200
@@ -9,7 +9,7 @@
 imports SPARK_Setup
 begin
 
-text {* Bitwise logical operators *}
+text \<open>Bitwise logical operators\<close>
 
 spark_proof_functions
   bit__and (integer, integer) : integer = "op AND"
@@ -54,7 +54,7 @@
   bit_not_spark_eq [where 'a=64, simplified]
 
 
-text {* Minimum and maximum *}
+text \<open>Minimum and maximum\<close>
 
 spark_proof_functions
   integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int"