On 8 Dec 2015,at 10:37, Anthony Fox <[email protected]> wrote: > I’m not sure if it makes sense to think about exporting the theory in such > a way that references to unsaved theorems are eliminated. Thibault Gauthier > is better placed to discuss this issue. >
I would say that references to unsaved theorems should be eliminated, but I think the dependencies of the unsaved theorem should be first added to the dependencies of the theorem that depended on that unsaved theorem. If otherwise the dependencies of the unsaved theorem are lost, it seems to me that dependencies on arbitrary axioms could be obfuscated by deleting the lemma that was using that axiom. Am I wrong? Andrea
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
