On 6/11/2012 2:29 PM, Konrad Slind wrote:
> Here's the change, which sets the fixity status of
> the identifier, then makes the definition.
>
> set_fixity "divides" (Infix(NONASSOC, 450));
>
> val divides_def =
> Define
> `a divides b = ?x. b = a * x`;
> Konrad.
That's good to know.
I got hol-mode.el running under Emacs, with the unicode working right.
http://ftp.gnu.org/gnu/emacs/windows/
The unicode didn't work with a Windows command console, so I had to
disable it.
Emacs is a lot better, including the HOL character highlighting, and the
X-windows part of XEmacs has never helped me figure out the many
mysteries of how to use Emacs.
Thanks again,
-GB
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
