On 23/06/11 13:54, mukesh agrawal wrote: > I am a new user to HOL . It would be really helpful if you let me > know about how to create a new simplification set like real_ss so > that I can use it with RW_TAC and other tacticals.
There is discussion of this in the relevant part of the Description Manual. See Section 5.5.3 "Simpset fragments" in particular. Basically, you should build new simpsets by using the ++ operator to add 'fragments' onto existing simpsets. For example: val my_ss = real_ss ++ ARITH_ss ++ rewrites [my_rwt1, my_rwt2] I hope this helps, Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Simplify data backup and recovery for your virtual environment with vRanger. Installation's a snap, and flexible recovery options mean your data is safe, secure and there when you need it. Data protection magic? Nope - It's vRanger. Get your free trial download today. http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
