[isabelle-dev] adhoc overloading
makarius at sketis.net
Thu May 30 23:08:45 CEST 2013
On Wed, 29 May 2013, Florian Haftmann wrote:
> Alternatively, use Context.>> directly in the body of the ML file
> (which, I guess, is nowadays preferred over explicit setup in the
> surrounding theory).
Hypersearch over the sources shows that Context.>> is still quite rare,
and there is no trend to be seen yet. Of course, a trend could be started
Last time we've discussed that privately, you were more in favour of setup
and I more in favour of Context.>> (quite some years ago).
I am myself used to Context.>> in Isabelle/Pure (there is no other way),
and I follow the old habit with 'setup' in Isabelle/HOL most of the time.
On the other hand, the received two-part idiom is a bit odd wrt. proper
Like two-component glue to be fit together by hand. It used to be three
components until recently, with extra "uses" in the theory header.
More information about the isabelle-dev