Megalodon 1.1

by Brown, Sunday, November 08, 2020, 17:27 (392 days ago)

I'm releasing Megalodon 1.1:

http://grid01.ciirc.cvut.cz/~chad/megalodon-1.1.tgz

It can be used to create Proofgold documents.

The main changes from 1.0 are that the default theory is Mizar (meaning, the Mizar style set theory in Proofgold) and there is now more general support for proofs by transitive chains of equal terms. If you're trying to prove s = t you can write

transitivity u1, u2, ..., un

and then there will be n+1 subgoals:

s = u1
u1 = u2
...
un = t

The Mizar theory Preamble is much bigger now, due to the many documents published in the past few months.