[isabelle-dev] Quotient.invariant

[Tobias Nipkow]

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:        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
> description:
> generation of a code certificate from a respectfulness theorem for constants
> lifted by the quotient_definition command & setup_lifting command: setups
> Quotient infrastructure from a typedef theorem
> 
> 
> It introduces a constant called "invariant" in main HOL.  It might be a
> candidate for "hide_const (open)".  Some experts on the Isabelle/HOL library can
> probably say more.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev