src/HOL/IMP/Hoare_Total_EX.thy
changeset 69505 cc2d676d5395
parent 68776 403dd13cf6e9
child 74500 40f03761f77f
--- a/src/HOL/IMP/Hoare_Total_EX.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/HOL/IMP/Hoare_Total_EX.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -91,7 +91,7 @@
 done
 
 
-text\<open>Function @{text wpw} computes the weakest precondition of a While-loop
+text\<open>Function \<open>wpw\<close> computes the weakest precondition of a While-loop
 that is unfolded a fixed number of times.\<close>
 
 fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn \<Rightarrow> assn" where