The following problem is still open:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-December/msg00138.html
Here is again the critical example that produces tons of messages:
lemma "(!!P. P::bool) ==> PROP P" by blast
It should be tried out in "isabelle tty", to avoid bombing any non-trivial
front-end (e.g. Isabelle/jEdit or batch build).
We have had various situations in the past where friendly warnings caused
a total failure of existence. There are some measures againts that, like
avoiding redundant messages in the first place, or guarding message output
by Context_Position.if_visible (and making sure that the flag is
maintained reliably, but this is often difficult).
In the case of blast this is not so obvious. Maybe Larry can figure out
why the proof reconstruction fails so badly. Somehow strip_Trueprop might
get involved: it looses the information about presence or absence of
Trueprop.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
