Re: [isabelle] residual subgoals



Hi Gergely,

> 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:

  <https://stackoverflow.com/a/25442787/4776939>

Isabelle2016 has changed some things with that respect. For example, you
can now write

  fix P
  assume "P x" for x

instead of

  fix P
  assume "âx. P x"

Cheers
Lars




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