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 blastDo 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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
