metamath-data-0.180-lp152.1.29 RPM for noarch

From OpenSuSE Leap 15.2 for noarch

This package contains Metamath data base files for several formal theories.
* set.mm – Logic and set theory database (see Ch. 3 of the Metamath book).
* nf.mm – Logic and set theory database for Quine's New Foundations set theory.
* hol.mm – Higher order logic (simple type theory) database.
* iset.mm – Intuitionistic logic database.
* ql.mm – Quantum logic database.
* demo0.mm – Demo of simple formal system (see Ch. 2 of the Metamath book).
* miu.mm – Hofstadter's MIU-system (see Appendix D of the Metamath book).
* big-unifier.mm – A unification stress test (see comments in the file).
* peano.mm – A presentation of Peano arithmetic by Robert Solovay.

Provides

• metamath-data

Requires

• metamath = 0.180-lp152.1.29
• rpmlib(CompressedFileNames) <= 3.0.4-1
• rpmlib(FileDigests) <= 4.6.0-1
• rpmlib(PayloadFilesHavePrefix) <= 4.0-1
• rpmlib(PayloadIsXz) <= 5.2-1

License

CC0-1.0 AND GPL-2.0-or-later

Changelog

* Fri Dec 20 2019 Aaron Puchert <aaronpuchert@alice-dsl.net>
  - Update to version 0.180.
    * MINIMIZE_WITH axiom trace now starts from current NEW_PROOF
      instead of SAVEd proof.
    * Make sure traceback flags are cleared after MINIMIZE_WITH.
    * Add url pointer to HELP WRITE SOURCE /SPLIT.
    * Clarify HELP WRITE SOURCE /REWRAP.
    * Add bug check info for user.
    * Use '|->' (not 'e.') as syntax hint for maps-to.
    * Remove extraneous </TD>.
    * Fix "line 0" in error msg when label clashes with math symbol.
    * Improve TOOLS> HELP INSERT, DELETE.
    * Change bug 1511 to error message.
    * Trigger Most Recent link on mmtheorems.html when there is a
      mathbox statement (currently set.mm and iset.mm).
    * Improve help for TOOLS> DELETE and SUBSTITUTE.
    * Change "htmlHome" in warnings to "htmlhome".
* Wed Sep 25 2019 Aaron Puchert <aaronpuchert@alice-dsl.net>
  - Update to version 0.178.
  - Update book to version 20190602.
  - Remove Windows executable from sources before building.
* Wed May 01 2019 aaronpuchert@alice-dsl.net
  - Update to version 0.177.
  - Update book to version 20190407.
  - Use man page from upstream now.
* Thu Apr 04 2019 aaronpuchert@alice-dsl.net
  - Change SPDX identifier to GPL-2.0-or-later, as README.TXT states.
* Tue Mar 19 2019 aaronpuchert@alice-dsl.net
  - Fix dependency versions - since the book has a different version,
    we need to be careful which version we refer to.
* Sat Mar 16 2019 aaronpuchert@alice-dsl.net
  - Fix version number.
* Sat Mar 16 2019 Jan Engelhardt <jengelh@inai.de>
  - Remove %if..%endif guards that do not change the build result.
  - Itemize the list in the description.
* Sat Mar 16 2019 aaronpuchert@alice-dsl.net
  - Update to version 0.175.
  - Update Metamath book to version 20190307.
  - Use date as version number for Metamath book, because it isn't
    versioned alongside the program.
  - Move source links into comments, as they aren't stable. They
    always point to the latest version, which isn't compatible with
    download_files service runs.
* Thu Mar 07 2019 aaronpuchert@alice-dsl.net
  - Update to version 0.174.
  - Package Metamath book separately.
* Tue Jan 08 2019 aaronpuchert@alice-dsl.net
  - Update to version 0.171.
* Mon Aug 06 2018 aaronpuchert@alice-dsl.net
  - Update to version 0.163.
  - Recommend data package, make it noarch.
* Sun Feb 04 2018 aaronpuchert@alice-dsl.net
  - Add a brief manual page.
  - Do not build LaTeX docs on SLES, because TeXlive doesn't seem up
    to the task there.
* Sun Feb 04 2018 aaronpuchert@alice-dsl.net
  - Update to version 0.161.
  - Also build documentation.
  - Package data base files separately.
* Tue Oct 24 2017 aaronpuchert@alice-dsl.net
  - Update version to 0.155.
* Wed Jul 19 2017 aaronpuchert@alice-dsl.net
  - Really update version to 0.146.
* Wed Jul 19 2017 aaronpuchert@alice-dsl.net
  - Update version to 0.146.
* Sat Apr 15 2017 aaronpuchert@alice-dsl.net
  - Update version to 0.139.
* Mon Oct 31 2016 aaronpuchert@alice-dsl.net
  - Initial release of the package base on version 0.130.

Files

/usr/share/metamath
/usr/share/metamath/big-unifier.mm
/usr/share/metamath/demo0.mm
/usr/share/metamath/miu.mm
/usr/share/metamath/peano.mm
/usr/share/metamath/ql.mm
/usr/share/metamath/set.mm

Generated by rpm2html 1.8.1

Fabrice Bellet, Tue Apr 9 11:50:38 2024