On Saturday, September 5, 2020 at 6:19:34 PM UTC-4 di gmail.com wrote:
> The Metamath -> MM0 importer already contains a feature for selecting
> which target theorems you want, so it has the same effect as using /extract
> on the source database first and then importing it. I've been using
On Saturday, September 5, 2020 at 11:56:58 PM UTC+2 Norman Megill wrote:
> On Saturday, September 5, 2020 at 2:46:44 AM UTC-4 Alexander van der
> Vekens wrote:
>
>> That's sound really great! I will try this new feature soon, using the
>> friendship theorem as "root"...
>>
>
> Good choice. I
