Object level implication in Isabelle/HOL

Question

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?

Answer 1

I think the short answer is: Use ==> whenever possible as it is easier to work with than -->.

That being said, you should not see ==> too often in the code you write.

1. When writing a Lemma, it is often nicer to use the assumes and shows syntax.
2. For intermediate steps with have there is a syntax with if: have "B" if "A" instead of have "B ==> A"
3. The meta implication can only be used at the top level, so if you have a predicate as argument to a function you cannot use ==> in that predicate.