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 > Local_Theory.subtarget_result.
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.
Makarius
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
