[isabelle] proving monotonicity



Hi all,

is there any difference in Isabelle\HOL the following two formulas:

1)    \<forall>x \<in>A.  P(x)
2)   \<forall>x.  x \<in> A --> P(x)

A is an inductive set.
I would like  to use the first solution within a coinductive definition.
I don't get any error if I use the second solution, but if I use the first one the coinductive definition fail to prove the monotonicity .

Any advice?

Thanks in advance for the collaboration.

Regards.

-T





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