[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result
makarius at sketis.net
Thu Jan 31 15:38:26 CET 2019
On 22/01/2019 22:24, Florian Haftmann wrote:
> as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
> seen Local_Theory.reset invocations are gone, conveniently replaced by
This looks clean and canonical. At least we have Local_Theory.reset out
of the way in visible Isabelle/ML tool implementations: it is still
present inside Local_Theory.close_target, though.
I wonder what happens when that is removed: presumably it requires a lot
of fine-tuning to make everything work again without that hidden reset.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev