Re: [isabelle] efficiency

"blast" should do the job.


Julien schrieb:
Hi All,

I am trying to prove a goal P knowing:

a implies P ; b implies P ;  c implies P ; a \/ b \/ c

Each term a, b and c are of the form u /\ v.
The conclusion P is of the form u /\ (x \/ y \/ z ...).
But this should not matter for the proof.

With small formulae, auto or force work. But otherwise they both never terminate.

Does anyone know what I should use instead of "auto" or "force" to solve this kind of goal ?
I tried safe but it is not better.

Thanks a lot,

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