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

Make it easy to make custom compsets

Open mn200 opened this issue 9 years ago • 1 comments

An interface to allow it easy to

  1. add definitions by default to a custom compset
  2. mark certain definitions as not to be added
  3. mark certain theorems as to be added

In other words, provide something that makes it easy to build a user-controlled version of the global compset that is used by EVAL.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

mn200 avatar Aug 04 '16 10:08 mn200

What is needed for this beyond what is already provided by computeLib's API?

xrchz avatar Aug 07 '25 11:08 xrchz