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:
> 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."
> - Gergely
This archive was generated by a fusion of
Pipermail (Mailman edition) and