Oops, I meant to say within HOL Light system.
Sorry if there is any confusion.
Regards,
Robert
On 21 May 2015 at 14:00, Robert White <[email protected]> wrote:
> Dear all,
>
>
> I wonder if there is a way I can use TAC for EQ_MP.
>
> I'm sorry I'm not very familiar with bottom up proofs.
>
> A1 |- t1 <=> t2 A2 |- t1'
> ----------------------------- EQ_MP
> A1 u A2 |- t2
>
> Thanks!
> --
>
> Regards,
> Robert
>
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
