[isabelle-dev] Quotient.invariant

Makarius makarius at sketis.net
Fri Mar 23 17:34:12 CET 2012

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 
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.


More information about the isabelle-dev mailing list