[isabelle-dev] adhoc overloading

Makarius 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 

   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.


More information about the isabelle-dev mailing list