> On December 1, 2019 2:24:25 PM PST, Benoit <[email protected]> wrote: > >Hi all, > > > >A few months ago, after the discussion here on bundling with Mario, I > >experimented removing dependencies on ax-13 from many theorems.
In general we encourage removing dependencies on axioms. I don't see why it would be different in this case. --- David A. Wheeler -- 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/E1ibdaQ-0003zI-QO%40rmmprod07.runbox.
