Re: [isabelle] trivial Isar proof fails



On 20/06/2014 14:25, Gergely Buday wrote:
> Tobias Nipkow wrote:
> 
>> It worked at the time (like 12 years ago) but systems change. Arbitrary
>> documents you find somewhere on the web have the tendency to be outdated.
> 
> What is an up-to-date tutorial for Isar then? What I have found was
> the Proofs chapter of the Isabelle/Isar Reference:
> 
> http://isabelle.in.tum.de/doc/isar-ref.pdf#page=118
> 
> but that is terse and dry for a beginner.

You have found the documentation directory but have chosen the reference manual.
Maybe you are looking for a tutorial? Then I recommend the first item in the
Tutorials section: "Programming and Proving in Isabelle/HOL."

Tobias

> - Gergely
> 




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