I've made Konrad's suggested change in the repository so that users of future releases won't hit the same problem.
You can see the revised file at https://raw.github.com/mn200/HOL/e8110e6d9c03e54685f30f216357f77ef380b8f2/examples/euclid.sml Best, Michael On 12/06/12 05:29, Konrad Slind wrote: >>> 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 ------------------------------------------------------------------------------ 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
