Re: [isabelle] trivial Isar proof fails



Hi Gergely,

Am 20.06.2014 um 12:35 schrieb Gergely Buday <gbuday at gmail.com>:

> on the bottom of page 3 of
> 
> http://arachne.it.uu.se/grad/courses/gc0910/isabelle/isar-overview.pdf#page=3
> 
> there is a proof
> 
> lemma "A ⟶ A"
> proof
>  assume "A"
>  show "A" .
> 
> introducing dot as a trivial proof. In my 2013-2 installation it does not work:
> 
> Failed to finish proof:
> goal (1 subgoal):
> 1. A
> 
> What is the problem here?

The overview seems wrong (or obsolete) there. If you replace the keyword "show" by "thus" (or "then show" or "from this show"), the assumption correctly gets chained into the goal, and "." works as expected.

Jasmin





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