Re: [isabelle] Isar tutorial example broken?

As Amine explained, modulo your typos, that proof used to work but
Makarius no longer liked that style and switched it off.


Chris Capel schrieb:
> 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. I'm using ProofGeneral. The preceding example, where the
> assumption is named and referenced with "by (rule a)" works. Is this
> something broken in the repository?
> Chris Capel

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