Re: [isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

2019-01-31 Thread Makarius
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

[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

2019-01-22 Thread Florian Haftmann
Hi all, 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. I'm considering pushing that even further: specification tools should by contract provide a »clean« definitional