Thank you very much. I will take a look a this tactic.
On Nov 5, 2012 4:27 AM, "Roger Bishop Jones" <r...@rbjones.com> wrote:
> 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);
Proofpower mailing list