Re: [isabelle] residual subgoals
> Is it standard practice not to bother these but postpone solving them via the final qed?
I'd say it's not standard practice. Most Isabelle users prefer not using
meta-implications and meta-quantification in Isar proofs if it can be
avoided. See Lars Noschinski's answer here for a case where it actually
doesn't work if you use meta-implication:
Isabelle2016 has changed some things with that respect. For example, you
can now write
assume "P x" for x
assume "âx. P x"
This archive was generated by a fusion of
Pipermail (Mailman edition) and