A couple of places to look in HOLindex: refuteLib and normalForms structure.
On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe) <[email protected]> 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 > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
