[isabelle-dev] adhoc overloading

[Makarius]

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 
now.

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 
modularity:

   ML_file "foo.ML"
   setup Foo.setup

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.


 	Makarius