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 <[email protected]> wrote: > 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/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. > > At this point it's not clear if this constant will be used only for internal > purposes. The original idea was to allow users to write definitions like this > one: > > quotient_type 'a foo = 'a bar / invariant P > > If it turns out that we need this constant only internally, it will be hidden. > > Ondrej > _______________________________________________ > 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
