[isabelle] universal quantifiers vs. schematic variables



if "P" is a previously defined predicate and I want to prove it always
holds, it seems I can do it in two ways. the first uses the universal
quantifier as in
    lemma "!x. P(x)"
    ....
and the second uses schematic variables, as in
    lemma  "P(x)"
    ...
if I'm not mistaken each of these can be used to prove the other, so they
are logically equivalent. the only differences I could find were in the way
the proved lemmas can be used in proofs, where usually the second
formulation is easier to use. my question is if this is indeed the case,
and if so why does Isabelle offer two different ways to say the same thing.
comparing to the case of --> and ==>, the different arrows are also
logically equivalent but they are intended for different situations, but I
couldn't find such distinction in the universal case.

thanx.



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