diff -r 52a87574bca9 -r 6c6ccf573479 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat Jan 02 18:48:45 2016 +0100
@@ -152,14 +152,14 @@
 
 text \<open>
   The next definition and three proof rules implement an algorithm to
-  enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
+  enumarate natural numbers. The command \<open>apply (elim pc_end pc_next pc_0\<close> 
   transforms a goal of the form
   @{prop [display] "pc < n \<Longrightarrow> P pc"} 
   into a series of goals
   @{prop [display] "P 0"} 
   @{prop [display] "P (Suc 0)"} 
 
-  @{text "\<dots>"}
+  \<open>\<dots>\<close>
 
   @{prop [display] "P n"} 
 \<close>