Hi Roger,

Thank you very much. Your solution works perfectly for me. Just be a little 
curious, what dose the following promoted message means when applying the tactic

        'Tactics proof introduced the subgoal 2 but did not request it as a 


> On 24 Sep 2015, at 18:13, Roger Bishop Jones <postmas...@rbjones.com> wrote:
> Yuhui,
> See attached a rough cut at what you were looking for.
> Roger Jones
> <cond_rewrite.doc>

We invite research leaders and ambitious early career researchers to 
join us in leading and driving research in key inter-disciplinary themes. 
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.

Proofpower mailing list

Reply via email to