aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorstuebinm2022-06-29 01:14:51 +0200
committerstuebinm2022-06-29 01:23:31 +0200
commitcb4139dc35527bd8c8f9b70753c3d1f552c5f19d (patch)
tree8e5709039197ad6d72d8b38235a982bf687e2608 /hott
parent5655750e12d3459c1237588f8dec3fc883a966b7 (diff)
make mltt work with isabelle 2021-1
notably, this modifies the proof method `this`: the previous version of it no longer works with cconv.ML (borrowed from HOL), so now it's just a call to the simplifier, which does work. Unfortunately the new `this` can otherwise do less than the old one (it does not instantiate schematic variables), so the old one is now available as `infer` instead.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions