Extend decimal point and Misc. (#2379)
Extend decimal point and Misc. (#2379)

* Decimal expansion and Misc.

* Reverting to the prefix notation for decimal expansion.

* Adding a link to the original mailing list discussion on decimal point.

* Fix typo and uncomment equality theorems
metamath/set.mm,metamath/set.mm,metamath/set.mm