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