Re: [isabelle] Isar tutorial example broken?
On Mon, 19 Jan 2009, Chris Capel wrote:
> I'm working through the isar tutorial by Tobias Nipkow, and didn't get
> very far before finding a problem.
> lemma "A --> A"
> assume "A"
> shows "A" .
> This example fails at the proof of shows, with an empty result
> sequence. I am using the repository version of isabelle with the HOL
> theory loaded, and my theory imports Main and doesn't do anything
It should work if you use the version of the tuturial from the same
Using assumptions implicitly is considered harmful for many years already
-- it stems from very early stage of Isar, where the exact relation to old
tactical proof style was not yet fully understood.
This archive was generated by a fusion of
Pipermail (Mailman edition) and