Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
Name: metamath-data | Distribution: SUSE Linux Enterprise 15 SP3 |
Version: 0.196 | Vendor: openSUSE |
Release: bp153.2.1 | Build date: Thu Mar 25 11:06:58 2021 |
Group: Productivity/Scientific/Math | Build host: lamb11 |
Size: 41976980 | Source RPM: metamath-0.196-bp153.2.1.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
* Wed Mar 03 2021 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 0.196. * Fix bug causing new axioms to be used by MINIMIZE_WITH. * Add "Claim" to bib ref types. * Remove error check for $e <- $f assignments. * Check for discouragement tags in *ALT, *OLD labels in VERIFY MARKUP. * Add underscore checking in VERIFY MARKUP and add /UNDERSCORE- _SKIP qualifier; also check for trailing space on lines. * Refine prevention of WRITE SOURCE.../REWRAP from modifying comments containing "<HTML>". * Allow space in TOOLS> BREAK. * Add checking for mathbox independence to VERIFY MARKUP; add /MATHBOX_SKIP. * "PROVE =" will now resume the previous MM-PA session if there was one; allow "~" to start/end with blank (meaning first/last statement); add "@1234". * Add /INCLUDE_MATHBOXES to to IMPROVE; notify user upon ASSIGN from another mathbox. * Print message when IMPROVE or MINIMIZE_WITH uses another mathbox. * Add CONJECTURE, RESULT to [bib] keywords. * Add HELP BIBLIOGRAPHY. * Added CONCLUSION FACT INTRODUCTION PARAGRAPH SCOLIA SCOLION SUBSECTION TABLE to [bib] keywords. * Added WRITE SOURCE ... /EXTRACT .... * Make the output of /EXTRACT stable in the sense that, with the same <label-list> parameter, extract(extract(file)) = extract(file) except that the date stamp at the top will be updated. (The first extraction even if "*" will usually be different because it discards non-relevant content. Note that the include file directives "$( $[ Begin..." etc. and comments with "$j" are currently discarded.) * Add keyword "htmlexturl" to $t statement in .mm file. * Prevent "htmlexturl" links from wrapping. * Temporarily disable /REWRAP until bug fixed. * Fix bug that deleted comments that were followed by ${, $}, $c, $v, $d on the same line. - Relax dependencies. * 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 Apr 9 14:50:04 2024