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" <[email protected]> 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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
