Re: [isabelle] problem with opening proof



Hi Chris,

>>> fix ...
>>> assume ... and ...
>>> thus "EX x y. ..."
>>> proof
>> "proof" is short for "proof default", where the "default" method performs:
> 
> In the Isar documentation it says "Unless given explicitly by the
> user, the default initial method is “rule”". Is this inaccurate?

Indeed, "default" is almost "rule", except if the proposition to prove
involves class or locale predicates;  this we can ignore here.

> But why does it also fail for "proof (rule exI)"? What's the
> difference between rule and intro that allows the latter to succeed?

"rule" performs introduction if no facts are chained in, and elimination
if some facts are chained in.  "intro" only performs introduction.

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.