Re: [isabelle] efficiency
"blast" should do the job.
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
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