[isabelle] --> vs. ==>



Hi,

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?

Thanks
Steve




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