On 22/10/17 13:04, Konrad Slind wrote: > Some of these are support for other proof infrastructure, but the main > theories give you booleans, products, sums, options, numbers, lists, > and sets. This is a useful basis on which to begin most formalizations.
Thanks. I thought “export_theory” computed the actual dependencies, as opposed to using all loaded theories indiscriminately. > […] Then you will have to explicitly load in all the needed tools and > theories. > For use of Holmake, I am pretty sure there is an option to support > hol.bare, but I am not sure what it is. There is the “--holstate” command line option of Holmake and the special variable HOLHEAP in a Holmakefile which can be used to employ the bare heap. But I do not know what is the preferred method. Regards. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
