On Sat, 24 Mar 2012, Ondřej Kunčar wrote:
The constant is now hidden.
Just two more things:
* "Now" means Isabelle/e64ffc96a49f -- The issue of proper references to
changesets is a running gag on isabelle-dev already. If you want, you can
make it the discriminating aspect between the two
On 03/24/2012 08:16 AM, Florian Haftmann wrote:
I would strongly vote for qualified access:
Quotient.invariant
9 keys more to type, but very self-explanatory.
Florian
The constant is now hidden.
Ondrej
___
isabelle-dev mailing list
I would strongly vote for qualified access:
Quotient.invariant
9 keys more to type, but very self-explanatory.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digit
If it turns out that the constant is not internal-only, it should get a more
specific name. "invariant" really is a name that should be available to users
without shadowing.
Cheers,
Gerwin
On 24/03/2012, at 4:06, Ondřej Kunčar wrote:
> On 03/23/2012 05:34 PM, Makarius wrote:
>> Just a note o
On 03/23/2012 05:34 PM, Makarius wrote:
Just a note on the following changeset:
changeset: 47095:3ea48c19673e
user: kuncar
date: Fri Mar 23 14:25:31 2012 +0100
files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotie
Absolutely, thanks. Constants should be hidden if they are internal to some
package. Especially with such a universal name as "invariant".
Tobias
Am 23/03/2012 17:34, schrieb Makarius:
> Just a note on the following changeset:
>
> changeset: 47095:3ea48c19673e
> user:kuncar
> date:
Just a note on the following changeset:
changeset: 47095:3ea48c19673e
user:kuncar
date:Fri Mar 23 14:25:31 2012 +0100
files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_type.ML
descr
