I think you can just write 510:,,500:syl2anc or 510:500,,:syl2anc
for that. On Wed, Jan 8, 2020 at 10:51 AM Jim Kingdon <[email protected]> wrote: > On 1/8/20 5:01 AM, Mario Carneiro wrote: > > > I would have completely removed the "?" but it breaks a lot of > > backward compatibility. It is currently only useful for the "step > > search": if you double click on "step:: |- foo" then it will search > > only for proofs of |- foo with no assumptions, and if you double click > > "step:?: |- foo" it will search for proofs of foo with possibly > > additional hypotheses. > > The ? is still useful in telling mmj2 which hypotheses to fill in. For > example, if I have a step 500 and I want to say > > 510:500:syl2anc > > and have mmj2 fill in the other two hypotheses. Before typing control-U > I can modify that to be: > > 510:?,?,500:syl2anc > > or > > 510:500,?,?:syl2anc > > before writing unify. > > I just tried this with mmj2 2.5.3 as of 23-Sep-2019 (as reported in the > About box). > > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/6ca7f932-4475-3dcc-d66b-d42c2296a63c%40panix.com > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuLn35B9-VTNQpzEmXmdGGmL%2BXhhjnbKJfytJ35OUWZug%40mail.gmail.com.
