search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

shorten wl version of cadan again #3996

Closed wlammen closed 3 months ago

wlammen commented 3 months ago
  1. mathbox: rename wl-3mintru2an -> wl-df-3mintru2-2, its an alternative definition, so name it as such.
  2. mathbox: comment changes
  3. mathbox: shorten wl-df-3mintru2-2 again (shorter than the copy cadan now)
  4. delete outdated OLD theorems.