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
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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