Roger,

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

Regards,
Jon
On Nov 5, 2012 4:27 AM, "Roger Bishop Jones" <r...@rbjones.com> 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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to