Re: [isabelle] About mem and set

This is the same behaviour as your last email. If you want the goal to be parsed as an If and only if, the bracket it, otherwise use the <--> symbol, it is = on bool with the usual prioities.

Of course x mem x is not a member of the empty set.

Cristiano Longo wrote:
I can prove the following lemma

"x \<in> {} = x mem []"

but, simplyfing this one

"x mem [] = x \<in> {}"

it results as False.

thanks in advance,
Cristiano Longo

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