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
