>> Send (or post) a minimal failing version and the maintainers can help
>> you.
>
> I thought it was me causing problems by loading my own scripts after
> "HOL/examples/euclid.sml", but it wasn't.
The failure comes from making the "divides" constant an infix after its
definition. All is fine the first time around, but the second time the file
is used, divides is encountered in prefix position, but is expected to be
in infix position. 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.
------------------------------------------------------------------------------
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
