Hol_reln seems to be creating names with "?" (I would have expected the name of the reln being defined instead of "?") and I can't figure out how to fix this. Help appreciated! -- Mike
lox% Holmake [stuff deleted] Saved theorem ?_rules Saved theorem ?_ind Saved theorem ?_cases <<HOL message: The following ML binding names in the theory to be exported: "?_rules", "?_ind", "?_cases" are not acceptable ML identifiers. Use `set_MLname <bad> <good>' to change each name.>> Uncaught exception: HOL_ERR lox% ------------------------------------------------------------------------------ Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
