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) <[email protected]> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
