Re: [isabelle] Isar tutorial example broken?

Chris Capel schrieb:

> lemma "A --> A"
>   assume "A"
>   shows "A" .
> qed

Note that fix*es*/ assume*s* / show*s* is just a different way to write
down propositions to prove.  What you probably meant was something like:

> lemma "A --> A"
> proof
>   assume "A"
>   then show "A" .
> qed

Something similar with assume*s*, show*s*:

> lemma
>   assumes A
>   shows A
> proof -
>   from assms show A .
> qed

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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