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" .
> qed
> 
> 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
> else.

It should work if you use the version of the tuturial from the same 
repository snapshot.

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.


	Makarius





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