Hi, Currently I’m doing several projects in HOL4, and fortunately Kananaskis-11 was finally released early this month, and for now I only use K-11 final release and not chasing and rebuild HOL from Git master any more. On the other side, I finally learnt to use PAT_X_ASSUM to “pop” any assumption I want, just like a more flexible version of POP_ASSUM.
My goal is to have my proof scripts being able to run in both K11 final release and current ongoing K12 versions, so when I need to “pop” an assumption, I always write it as PAT_X_ASSUM and having this line in all my *Script.sml files: (* This is for Kananaskis 11 only, remove it for K12. *) val PAT_X_ASSUM = PAT_ASSUM; The question is, at PolyML (and MosML) level, how to write code to re-define PAT_X_ASSUM only in K11 final release (and before)? Or there’s another better solution to this entire problem? Regards, Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
