[isabelle] Confusing behavior of a paired set comprehension



Hello,
the following definition is interpreted in a confusing way:

def ident :: "'a set => ('a \times 'a) set"
where "ident S = {(x,x) . x \in S}"

the command "thm ident_def" yields
ident ?S \<equiv> {(xa, x). x \<in> ?S}

Should this be considered as a bug?

Giuliano




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.