HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
621 stars 140 forks source link

Add to sptree compset #1178

Closed xrchz closed 8 months ago

mn200 commented 8 months ago

It'd be great if you could extend the selftest.sml to test this new functionality.

mn200 commented 8 months ago

Awesome thanks!