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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
