I see that many theorems in Isabelle/HOL prefer meta-level implication:
==>
instead of
-->
the object logic level, i.e. higher order logic implication.
Isabelle wiki says that roughly speaking, meta level implication should be used to separate the assumptions from the conclusion in rule statements.
Other than that, what should I know about the use of object and meta level implication? I see the latter is being used mostly. When and for what should I use HOL implication?