<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">What is the status of things like let-terms and set comprehensions in the Gilith Open Theory Repo. I can't see the definitions of the magic constants that are used to represent these things (LET and GSPEC in HOL Light and HOL4)? A peculiar sequence of complicated assumptions involving let builds up in the HTML listings.<div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>