aboutsummaryrefslogtreecommitdiff
path: root/Eq.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Syntax changes. Transport inverse lemmas.Josh Chen2019-03-011-18/+70
* more convenient syntaxJosh Chen2019-02-281-68/+91
* 1. Remove all type inference functionality (feature development moving to ano...Josh Chen2019-02-281-53/+163
* more proofs involving equalityJosh Chen2019-02-231-44/+97
* rewrite associativity proofJosh Chen2019-02-231-17/+16
* Cleanups and reorganizationJosh Chen2019-02-221-10/+17
* Proof of pathcomp associativity done. Some commentsJosh Chen2019-02-221-0/+229