Re: [isabelle] --> vs. ==>

The connective ==> is part of the logical framework, and is not part of higher-order logic at all. Therefore, the expression A ==> B is not a higher-order logic formula and cannot be written where a formula is expected, such as a set comprehension.

Larry Paulson

On 6 Aug 2010, at 05:23, Steve W wrote:

> I see that both --> and ==> mean implication, whereas the first is the
> logical connective and the second is for inference rules. However, can a HOL
> formula containing --> be proved as one with ==> instead? It seems it
> doesn't make much difference as impI replaces --> by ==>. My feeling is that
> it's not safe to replace --> with ==>, but what really are the issues?

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