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.

0 files changed, 0 insertions, 0 deletions