[isabelle] Understanding backtracking in by vs qed



Dear Isabelle list,

I have a proof that works:

   have <statement> using <facts>
   proof (move, infer_ty) qed (auto simp: ty)

and one that doesn't:

   have <statement> using <facts>
   by (move, infer_ty) (auto simp: ty)

The manual says that "by" abbreviates "proof ... qed" but with additional backtracking, what is it about this that could cause "by" to fail and "qed" to succeed?

I'm unsure if it would be relevant, but infer_ty is a method that only changes the proof context (by adding some theorems to context data) without changing the goal.

Best,
Josh




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