--- a/src/Doc/IsarRef/HOL_Specific.thy Thu Mar 06 15:25:21 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Thu Mar 06 15:29:18 2014 +0100
@@ -1565,7 +1565,7 @@
using the same attribute. For example:
@{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
- @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (prod_rel A B)"}
+ @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
\item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
of rules, which specify a domain of a transfer relation by a predicate.