aboutsummaryrefslogtreecommitdiff
path: root/Coprod.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2018-08-16Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen1-1/+1
2018-08-16Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen1-1/+1
2018-08-14Well-formation rules are back in the methods; new theory synthesizing the nat...Josh Chen1-5/+9
2018-08-12Commit before testing polymorphic equality eliminatorJosh Chen1-5/+5
2018-08-07Old application syntax incompatible with EisbachJosh Chen1-20/+20
2018-08-04CoproductJosh Chen1-0/+61