summaryrefslogtreecommitdiff
path: root/PL.v
AgeCommit message (Expand)Author
2021-04-20Many changes to PL.v file, proved PM axiomsHEADmasterLandon D. C. Elkind
2021-03-31Proved PM axioms using Coq's classical librariesLandon D. C. Elkind
2021-02-14Proof of *5.7 now follows PM sketchLandon D. C. Elkind
2021-02-05Added theorem namesLandon D. C. Elkind
2021-02-03Deleted superseded files, fixed typosLandon D. C. Elkind
2020-12-31PL completely checkedLandon D. C. Elkind