Re: [isabelle] trivial Isar proof fails
Am 20.06.2014 um 12:35 schrieb Gergely Buday <gbuday at gmail.com>:
> on the bottom of page 3 of
> there is a proof
> lemma "A ⟶ A"
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and