El 31/07/20 a las 11:35, Mario Xerxes Castelán Castro «Ksenia» escribió: > That is the case relevant at hand, where the equation is buried in an > implication because the function is only partially defined. Is there a > standard way to deal with this?
I made a pull request to add support of this case to computeLib: <https://github.com/HOL-Theorem-Prover/HOL/pull/863>. _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
