aboutsummaryrefslogtreecommitdiff
path: root/ex/HoTT Book/Ch1.thy
diff options
context:
space:
mode:
authorJosh Chen2018-08-14 17:43:03 +0200
committerJosh Chen2018-08-14 17:43:03 +0200
commite6473c383b479610cee4c0119e5811a12a938cf9 (patch)
tree477ecc678909b6e29e064ede72b9dee0933c58ad /ex/HoTT Book/Ch1.thy
parentf83534561085c224ab30343b945ee74d1ce547f4 (diff)
Well-formation rules are back in the methods; new theory synthesizing the natural number predecessor function.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions