[isabelle-dev] copying contexts

Lucas Dixon ldixon at inf.ed.ac.uk
Wed Dec 2 13:16:21 CET 2009


I'm wondering what the right way to copy contexts is. I remember there
was some references lingering in theories, mostly as unique identifies
if I remember correctly, but it meant that copying needed to be an
explicit function. Is this the right way to copy a context:

Context.map_theory Context.copy_thy

and so copying a proof context would be:

Context.proof_map (Context.map_theory Context.copy_thy)


The reason I want to do this is that when proof planning proves new
theorems it creates some meta-data which gets stored in the context. I
want to be able to make a copy the context before I modify any such data
so that I can compare alternatives and do fair tests. I was previously
using my own generic context, but would like to cut down code duplication.


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

More information about the isabelle-dev mailing list