aboutsummaryrefslogtreecommitdiff
path: root/hott/Nat.thy
diff options
context:
space:
mode:
authorJosh Chen2020-05-30 18:29:11 +0200
committerJosh Chen2020-05-30 18:29:11 +0200
commit68bbcdcca00ae85dcaeae3ba7858dff1aa4802a6 (patch)
tree94678c24c0e6e7eeb41cb85f9053cd03c4d1b697 /hott/Nat.thy
parent2e807b74bd0f4e9a2ccfcb861bef876dba5aa066 (diff)
inhabitation coercion should be syntax, not logical constant!
Diffstat (limited to 'hott/Nat.thy')
0 files changed, 0 insertions, 0 deletions