Re: [isabelle] Questions about speed and CPU usage



> Btw. I like the Structured Isar Proofs much more than that other one with
> "apply" etc., because that actually allows me to consciously prove (at least
> very simple) things whereas that other looks like randomly trying different
> buttons in hope that they eventually do something [this was actually why I
> switched to Isabelle after playing with Coq a few days that I saw that
> manual and it's just nice]. Structured proofs is clearly at least a good
> starting point, but this goal-based way is nice in many ways (I wish that
> most library proofs were built in that way).

Since you are still learning, you might also be interested in the slides
of my Isabelle course:
http://isabelle.in.tum.de/coursematerial/PSV2009-1/index.html
It starts off with "apply" but later it introduces structured proofs
through proof patterns that may help.

Tobias





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