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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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