aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Library organization and formattingJosh Chen2018-06-271-1/+3
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...Josh Chen2018-06-181-2/+1
* Removed all [simp] attributes, these will be added later when I set up the si...Josh Chen2018-06-181-1/+1
* Proof of projection functions now harder. Should look up automation methods.Josh Chen2018-06-171-1/+1
* projectionsJosh Chen2018-06-151-27/+13
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-15/+29
* Reorganize codeJosh Chen2018-06-091-0/+52