aboutsummaryrefslogtreecommitdiff
path: root/Nat.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2018-08-17CleanupsJosh Chen1-4/+4
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-14Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen1-0/+5
natural number predecessor function.
2018-08-14Equality inverse and composition done. Cleaned up methods and method example ↵Josh Chen1-1/+1
theory.
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