I have written this
<http://hg.gnu.org.ua/hgweb/hol-proofs/file/e6bbb023cfb9/pfunScript.sml>
HOL4 theory that introduces a new type for partial (with respect to the
universe of the type) functions. The script file is tiny and trivial,
but at least it can save the time to type it to somebody else; it can be
reused as it is under a free license (GNU GPL 3 or later).
Regards.
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
