Hello, I have found that the current development snapshot (2010-01-10) and version 2.20 of HOL Light behave differently concerning the assumptions in SET_TAC. Assume the following example:
g(`~(x:num = y) /\ ~(x IN a DELETE y) ==> ~(x IN a)`);; Then SET_TAC[] solves it immediately in both versions. However, if we do also e(REPEAT STRIP_TAC);; then SET_TAC[] solves the goal in 2.20 but not in the current version. Is it a bug or it's the feature? If so, is there a way how to tell SET_TAC to use assumptions? Peter ------------------------------------------------------------------------------ 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
