[isabelle] proving monotonicity
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 .
Thanks in advance for the collaboration.
This archive was generated by a fusion of
Pipermail (Mailman edition) and