Hi… thanks, but it doesn’t work in HOL K11 final (where PAT_X_ASSUM is not defined):
--------------------------------------------------------------------- HOL-4 [Kananaskis 11 (expknl, built Tue Mar 07 09:23:36 2017)] For introductory HOL help, type: help "hol"; To exit type <Control>-D --------------------------------------------------------------------- > val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM; poly: : error: Value or constructor (PAT_X_ASSUM) has not been declared Found near if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM Static Errors > Il giorno 25 mar 2017, alle ore 04:02, Ramana Kumar <ram...@member.fsf.org> > ha scritto: > > One thing you could try is to use Globals.version, e.g., > val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM; > > On 25 March 2017 at 07:32, Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > 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 > > > ------------------------------------------------------------------------------ > 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 > >
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