Isabelle-HoTT/mltt, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 https://stuebinm.eu/git/Isabelle-HoTT/atom/mltt?h=master 2022-06-28T23:23:31Z make mltt work with isabelle 2021-1 2022-06-28T23:23:31Z stuebinm 2022-06-28T23:14:51Z urn:sha1:cb4139dc35527bd8c8f9b70753c3d1f552c5f19d 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. 1. Thm/def statement display. 2. Syntax + computation proof. 2021-06-28T15:06:19Z Josh Chen 2021-06-28T15:06:19Z urn:sha1:5655750e12d3459c1237588f8dec3fc883a966b7 Bad practice huge commit: 2021-06-24T21:40:05Z Josh Chen 2021-06-24T21:40:05Z urn:sha1:f988d541364841cd208f4fd21ff8e5e2935fc7aa 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file 1. Put universe level parameters first in automatic term definitions. 2. Add debugging to typechecker 2021-06-23T15:26:23Z Josh Chen 2021-06-23T15:26:23Z urn:sha1:0085798a86a35e2430a97289e894724f688db435 Merge branch 'dev' 2021-04-17T16:41:56Z Josh Chen 2021-04-17T16:41:56Z urn:sha1:75ab44cc1d2ad63864ecb43215a56538748fc0d3 Small fix: extraneous variable 2021-04-17T16:16:45Z Josh Chen 2021-04-17T16:16:45Z urn:sha1:3a34ca2b43fbd5725a7435dfafdb4cf179a8ec8b small rename 2021-04-10T21:06:24Z Josh Chen 2021-04-10T21:06:24Z urn:sha1:54df7336797dfa07124652a9eb75aac978a1a359 rename things + some small changes 2021-01-31T02:54:51Z Josh Chen 2021-01-31T02:54:51Z urn:sha1:2feb56660700af107abb5a28a7120052ac405518