Re: [isabelle] Two questions of a beginner



Am 20/01/2013 15:07, schrieb Makarius:
> On Fri, 18 Jan 2013, Not Sure wrote:
> 
>> 1. blast, auto, ... are all GREAT!
>> But is there a way (in ProofGeneral) to see the proofs found by these
>> tools more detail?
> 
> Side note: You should definitely try Isabelle/jEdit instead of Proof General.
> 
> I've myself been substantially involved in making Isabelle Proof General work 13
> years ago, but I don't see any reason left to use it today (only habits of Emacs
> users that have to be unlearned.)

AFAIK, jedit does not

- show you if the lemma you have just stated is already proved in the context
- show you a counterexample (auto quickcheck) to a lemma you stated
- forces you to wait until sledgehammer has returned before you can scroll
around - otherwise s/h is interrupted and restarts.

The first two are particularly relevant for beginners.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.