aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/ml/lib.ML
diff options
context:
space:
mode:
authorstuebinm2022-06-29 01:28:53 +0200
committerstuebinm2022-06-29 01:28:53 +0200
commit4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d (patch)
tree2819976f3fe60d2e9796ec37d2b0736df55daa59 /spartan/core/ml/lib.ML
parentcb4139dc35527bd8c8f9b70753c3d1f552c5f19d (diff)
(broken) update hott for Isabelle 2021-1HEADmaster
this just replaces all instance of `this` with instances of `infer`. Unfortunately, it looks likes something else also broke, and I have no idea what it is (but the proof for equiv_if_equal fails). Sadly this means we can't get to univalence for now … (but rn I'm too tired to try anything else with it)
Diffstat (limited to 'spartan/core/ml/lib.ML')
0 files changed, 0 insertions, 0 deletions