A couple of places to look in HOLindex: refuteLib and normalForms structure.
On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > Hi, > > it can be proven (by DECIDE_TAC) that, > > |- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x > > but is there any conversion function available in HOL4 such that from LHS > of above equation I can directly get the RHS - something like a canonical > form? > > --Chun > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
