search

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
615 stars 133 forks source link

compsets should become functional #620

Open mn200 opened 5 years ago

mn200 commented 5 years ago

The references hidden inside compsets make manipulating them a pain. They also make concurrent operation hard.

konrad-slind commented 5 years ago

Agreed. I was never able to argue Bruno out of the ref. --Konrad.

On Fri, Nov 30, 2018 at 8:42 PM Michael Norrish notifications@github.com wrote:

The references hidden inside compsets make manipulating them a pain. They also make concurrent operation hard.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/620, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD1iaEu7CJQ15dACL2L1hCD47B47eks5u0ex7gaJpZM4Y8rHq .