On Wed, 28 Mar 2012, Ondřej Kunčar wrote:
After a long discussion during a lunch break we decided to use
".rep_eq". I will also change "_rsp" to ".rsp". What about "_def"?
Should I change it to ".def" as well? "_def" seems to be a
inconsistency, I guess because of historical reasons. Should new
packages use ".def" instead of "_def"?
I don't see a reason for ".def" -- the traditional "_def" still does its
job. By convention it somehow refers to a basic definition behind the
scenes, which is sometimes public, sometimes considered private.
BTW, qualified bindings do work in general, but not for term entities.
So a Local_Theory.define with qualified names will not exactly work as
could be expected, although that is its normal hevaiour: to regard only
the base name in the auxiliary context. So local term definitions of some
"foo.make" and "bar.make" will cause an error.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
