[opentheory-users] Status of derived syntax

[Rob Arthan]

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.

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131122/6150de2a/attachment.html>