[isabelle] Incomplete goal may cause proof methods of later goals to loop.
I'd expect the following issue to be well known but didn't find it in
the "known issues".
When inserting a new goal (have ...) into a proof, proof methods
belonging to later goals seem to be applied wrongly sometimes causing
them to loop and make my PC noisy after a while. ;)
Here's a small example:
lemma assumes "m ∈ M" and "M ⊆ N" shows "m ∈ N" proof -
have P(* incomplete goal *)
show "m ∈ N" using assms by (metis in_mono) (* loops *)
The "show" already produces a syntax error but the later "by" is applied
anyhow yet to the wrong goal causing it to loop.
A student of mine is highly skilled in producing such situations in many
theorems simultaneously causing the editor to become very unresponsive.
This archive was generated by a fusion of
Pipermail (Mailman edition) and