aboutsummaryrefslogtreecommitdiff
path: root/Nat.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2019-03-08some options, renamingJosh Chen1-1/+1
2019-02-22Cleanups and reorganizationJosh Chen1-24/+21
2018-09-19Not sure what advantage is provided by having eta-expanded forms in the rules...Josh Chen1-3/+3
2018-09-18Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...Josh Chen1-0/+1
2018-09-17Reorganizing theoriesJosh Chen1-33/+27
2018-09-11Go back to higher-order application notationJosh Chen1-14/+14
2018-08-18Reorganize methodsJosh Chen1-1/+1
2018-08-18Regrouping type rulesJosh Chen1-10/+9
2018-08-17CleanupsJosh Chen1-4/+4
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-0/+5
2018-08-14Equality inverse and composition done. Cleaned up methods and method example ...Josh Chen1-1/+1
2018-08-13rcompose doneJosh Chen1-0/+1
2018-08-07Old application syntax incompatible with EisbachJosh Chen1-15/+15
2018-08-06Partway through changing function application syntax style.Josh Chen1-0/+49
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 17:07:51 +0000