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
