aboutsummaryrefslogtreecommitdiff
path: root/Nat.thy
diff options
context:
space:
mode:
authorJosh Chen2018-08-07 00:05:38 +0200
committerJosh Chen2018-08-07 00:05:38 +0200
commitfdecdc58f50bdc4527eb7c10e37651e5fd9690aa (patch)
tree4e9f99516ae763fa0c02e88018f680dc979fe5fb /Nat.thy
parent4bab3b7f757f7cfbf86ad289b9d92b19a987043a (diff)
Experiment with polymorphic dependent eliminators, i.e. we leave type and type family decorations implicit.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions