[isabelle] --> vs. ==>


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.