Closed benjub closed 2 years ago
Because of a script used a metamath/set.mm removing "vprint" lines, these "vprint" lines must not be multilines.
Because of a script used a metamath/set.mm removing "vprint" lines, these "vprint" lines must not be multilines.