Hi list, in HOL4, I am trying to compile some utility files (i.e., they do not contain any theory, only SML functions).
An attempt with Holmake complains as follows: /.../.../.../ > Holmake Compiling bla.sml File "bla.sml", line 4, characters 0-9: ! structure S = ! ^^^^^^^^^ ! Syntax error. So the problem seems to be that I am defining a structure inside my utility files. Can Holmake deal with this? For information, I use MoscowML 2.10. Thanks! V. -- Dr Vincent Aravantinos Analysis and Design of Dependable Systems fortiss GmbH <www.fortiss.org/en> Guerickestrasse 25 | 80805 Munich | Germany ------------------------------------------------------------------------------ Android is increasing in popularity, but the open development platform that developers love is also attractive to malware creators. Download this white paper to learn more about secure code signing practices that can help keep Android apps secure. http://pubads.g.doubleclick.net/gampad/clk?id=65839951&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
