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