Hello everyone,
suppose I have a custom tactic that depends on a list of terms and I
want to keep adding elements to the list throughout my development.
I tried to achieve this using a :term list ref on the ML level. However,
it is the case that if I add some term in theory A and inspect the list
in theory B, where A is in the theory graph before B, all elements added
in A are not in the list anymore.
Can someone give me a hint on why this is the case or tell me a better
way to "share" a list of terms from a theory with theories depending on it?
Cheers,
Heiko
------------------------------------------------------------------------------
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
