| changeset 69593 | 3dda49e08b9d |
| parent 67717 | 5a1b299fe4af |
| child 74974 | 7733c794cfea |
--- a/src/HOL/Library/While_Combinator.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/HOL/Library/While_Combinator.thy Fri Jan 04 23:22:53 2019 +0100 @@ -209,7 +209,7 @@ text \<open> - The proof rule for @{term while}, where @{term P} is the invariant. + The proof rule for \<^term>\<open>while\<close>, where \<^term>\<open>P\<close> is the invariant. \<close> theorem while_rule_lemma: