On 12/03/10 06:26, Mike Gordon wrote: > 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
What does the inductive definition source text look like? My guess is that your parse has been messed up and Hol_reln really does think you are trying to (re-)define exists, i.e., "?". Hol_reln already checks for attempts to redefine /\, \/ and !; I'll get it to check for ? too. Michael ------------------------------------------------------------------------------ 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
