[isabelle-dev] blast warnings

[Makarius]

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