| changeset 69593 | 3dda49e08b9d |
| parent 61799 | 4cf66f21b764 |
| child 75624 | 22d1c5f2b9f4 |
--- a/src/HOL/BNF_Wellorder_Relation.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/HOL/BNF_Wellorder_Relation.thy Fri Jan 04 23:22:53 2019 +0100 @@ -22,7 +22,7 @@ begin text\<open>The following context encompasses all this section. In other words, -for the whole section, we consider a fixed well-order relation @{term "r"}.\<close> +for the whole section, we consider a fixed well-order relation \<^term>\<open>r\<close>.\<close> (* context wo_rel *)