| changeset 69593 | 3dda49e08b9d |
| parent 69313 | b021008c5397 |
| child 69712 | dc85b5b3a532 |
--- a/src/HOL/Library/Disjoint_Sets.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/HOL/Library/Disjoint_Sets.thy Fri Jan 04 23:22:53 2019 +0100 @@ -234,7 +234,7 @@ subsection \<open>Partitions\<close> text \<open> - Partitions @{term P} of a set @{term A}. We explicitly disallow empty sets. + Partitions \<^term>\<open>P\<close> of a set \<^term>\<open>A\<close>. We explicitly disallow empty sets. \<close> definition partition_on :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool"