Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
Name: metamath-data | Distribution: openSUSE Leap 15.2 |
Version: 0.180 | Vendor: openSUSE |
Release: lp152.1.29 | Build date: Tue Jun 9 07:56:37 2020 |
Group: Productivity/Scientific/Math | Build host: sheep88 |
Size: 37336710 | Source RPM: metamath-0.180-lp152.1.29.src.rpm |
Packager: https://bugs.opensuse.org | |
Url: http://us.metamath.org/ | |
Summary: Data base files for metamath |
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.
CC0-1.0 AND GPL-2.0-or-later
* 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.
/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 Jul 9 11:27:19 2024