HOL icon indicating copy to clipboard operation
HOL copied to clipboard
verified publisher icon HOL-Theorem-Prover

Implement SPECL in the kernel

Open ordinarymath opened this issue 4 months ago • 0 comments

SPEC_ALL is extremely slow for large terms. Using Thm.Specialize which will use lazy beta conv only helps the standard kernel. Given that GENL is already in the kernel I don't see why SPECL can't be.

ordinarymath avatar Sep 06 '25 05:09 ordinarymath