aboutsummaryrefslogtreecommitdiff
path: root/mltt/core/MLTT.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* make mltt work with isabelle 2021-1stuebinm2022-06-291-5/+10
* 1. Thm/def statement display. 2. Syntax + computation proof.Josh Chen2021-06-281-6/+6
* Bad practice huge commit:Josh Chen2021-06-241-23/+25
* 1. Put universe level parameters first in automatic term definitions. 2. Add ...Josh Chen2021-06-231-3/+0
* Merge branch 'dev'Josh Chen2021-04-171-1/+1
|\
| * Small fix: extraneous variableJosh Chen2021-04-171-1/+1
* | small renameJosh Chen2021-04-101-3/+3
|/
* rename things + some small changesJosh Chen2021-01-311-0/+569