[isabelle-dev] [isabelle] the sound of a sledgehammer

[Lawrence Paulson]

I certainly agree, sometimes that is exactly what you want to do.

Another idea is to implement sledgehammer a pop-up window tied to a particular place, which eventually will receive sledgehammer's result. Then you could continue editing the document freely, without interfering with the sledgehammer execution.

Larry

On 14 Feb 2013, at 17:34, Peter Lammich <lammich at in.tum.de> wrote:

> On Do, 2013-02-14 at 17:22 +0000, Lawrence Paulson wrote:
>> In a dream scenario, one might imagine opening a document containing a number of occurrences of "sorry", and each one of these occurrences would be given to counterexample finders and to sledgehammer, without any specific user intervention. Then somehow any counterexamples or proofs that were found would be noted somehow, and the user could inspect these.
>> 
>> I recognise this idea isn't even half baked. But I know that you want to look at these problems differently from just saying, "how did it work in Proof General"? And the idea of having a whole bunch of gaps checked (as it were) simultaneously is very appealing.
>> 
> 
> But both in jEdit and PG, there is one "gap" that the user is currently
> interested in most, and that's the proof he's currently editing viz. the
> lemma he has just typed. Unlike the document model of Isabelle/jEdit,
> the user that develops a theory file only works at one place in the file
> at the same time, and pays special interest to this place.
> As a user who just typed in/altered a lemma, I'm interested in a
> counter-example for that lemma --- without needing to type quickcheck,
> sledgehammer, or sorry first (I usually want to type proof, by, or apply
> there). 
> 
> 
> --
>  Peter
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev