Re: [isabelle] Implicit typing in lemma



Hi Steve,

> consts
> a :: real
> 
> axioms
> ax1: "f a = 0"
> 
> lemma lemma1: "EX func arg. func arg = 0"
> proof -
>   show "g a = 0"
>     using ax1
>     by auto
> qed

This will not work since the proof constructed in the proof ... qed body
(by means of "fixes", "assumes", "shows" -- only the latter present in
this example) does not match the outer proposition.

Hope this helps
	Florian

-- 

Home:
http://www.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.