aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy
diff options
context:
space:
mode:
authorJosh Chen2019-02-10 03:16:51 +0100
committerJosh Chen2019-02-10 03:16:51 +0100
commit29068d381a8b5d95c7fd4dc6111dcfb3a181f0bd (patch)
tree33e6c5614f7bd29bf0e66292b3122b5d414c7a7d /Prod.thy
parentafef9e63cb11267dc69b714a8b76415d75e2dd37 (diff)
Explicit references in antiquotations in typing.ML. Move trace switch definition to HoTT_Base.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions