--- 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>