aboutsummaryrefslogtreecommitdiff
path: root/hott/Nat.thy
diff options
context:
space:
mode:
authorJosh Chen2020-04-02 23:27:06 +0200
committerJosh Chen2020-04-02 23:27:06 +0200
commit2781c68f0fdb435827097efc497c2172d6050e50 (patch)
tree4f0e05000a490b9b9e33e8d082d96bfd5d83152f /hott/Nat.thy
parent0ddab0fe11c33fc559fc8fb58528618efdbc93a4 (diff)
1. make id function an abbrev. 2. fix reduce method
Diffstat (limited to 'hott/Nat.thy')
0 files changed, 0 insertions, 0 deletions