Re: [isabelle] trivial Isar proof fails



It worked at the time (like 12 years ago) but systems change. Arbitrary
documents you find somewhere on the web have the tendency to be outdated.

Tobias

On 20/06/2014 12:46, Jasmin Christian Blanchette wrote:
> 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.