[isabelle-dev] Quick and dirty update of theory ?
obua at in.tum.de
Mon Aug 27 15:56:42 CEST 2007
I have the following setup:
(1) a theory "lemmas.thy"
(2) some ML-code that uses this theory and that is loaded and executed
after the theory has been loaded
(3) some additional ML-code that defines a function f
I now use f and suddenly I notice that I have to update lemmas.thy by
for example adding another lemma to it (I dont take anything out of the
theory, but just add to it). Reloading lemmas.thy via 'use_thy "lemmas"'
works. But then a call to the function f returns the error message
*** Exception- ERROR "Different versions of theory component \"lemmas\""
well, that is to be expected, but reloading (2) costs me about 15
minutes (and raising), but is not really necessary. Does anybody know of
some hack (possibly in connection with the quick_n_dirty flag) to
circumvent above error message ?
More information about the isabelle-dev