HOL
HOL copied to clipboard
Speed up the simplifier caching of decision procedures.
This issue is about speeding up the code in src/simp/src/Cache.sml which is causing performance problem in large theories. The solution could be a more efficient algorithm or a cache eviction policy preventing the cache from getting too large or resetting the cache more often.