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
subgoal"
best,
Yuhui
> On 24 Sep 2015, at 18:13, Roger Bishop Jones <[email protected]> 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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
