Thank you very much. I will take a look a this tactic.

On Nov 5, 2012 4:27 AM, "Roger Bishop Jones" <> wrote:

> Jon,
> I should have mentioned that the problem goal you are
> looking at can be solved by linear arithmetic so you don't
> need any lemma at all.
> Linear arithmetic is not covered by the tutorlal but this is
> one way to prove the goal:
> a (PC_T1 "z_lin_arith" asm_prove_tac[]);
> Roger
Proofpower mailing list

Reply via email to