[isabelle-dev] Quotient.invariant

[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