Make it so that RM get optimized to take in 3 args in PolyML#1776
Open
ordinarymath wants to merge 1 commit intoHOL-Theorem-Prover:developfrom
Open
Make it so that RM get optimized to take in 3 args in PolyML#1776ordinarymath wants to merge 1 commit intoHOL-Theorem-Prover:developfrom
ordinarymath wants to merge 1 commit intoHOL-Theorem-Prover:developfrom
