cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard
verified publisher icon CakeML

Remove redundant uses of prove_case_eq_thm

Open ordinarymath opened this issue 4 months ago • 0 comments

Most of it can be done by using TypeBase.case_eq_of or using the sml bindings.

ordinarymath avatar Sep 08 '25 03:09 ordinarymath