[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML

[Makarius]

On Tue, 12 Apr 2016, Lawrence Paulson wrote:

> A relevant past message.

We have more messages in the archives, about blast ignoring the 
distinction of Trueprop vs. non-Trueprop propositions. This boils down to 
the following example, which is non-terminating in Isabelle2016 and 
current Isabelle/8b85a554c5c4:

lemma "(⋀P. P::bool) ⟹ PROP P" by blast


Do you still have a sense of your own src/Provers/blast.ML? It might be an 
easy exercise with our fine ML IDE to brush it up a little bit.


>> Date: 27 October 2014 at 20:22:02 GMT
>> http://stop-ttip.org  743,200 people so far

About 3 million further people have virtually joined that initiative, and 
there is another chance to participate physically, with A. Merkel and
B. Obama: http://www.ttip-demo.de


 	Makarius