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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
