I should read the docs first... In the new version, ASM SET_TAC[] does what SET_TAC[] did in 2.20. Now I love HOL Light even more. Peter
> 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
