*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 27 Oct 2009 20:26:16 +0100*In-reply-to*: <4AE5D661.2080708@uni-muenster.de>*References*: <4AE5D661.2080708@uni-muenster.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Quoting Peter Lammich <peter.lammich at uni-muenster.de>:

there are two ways of defining lattices in Isabelle: The first approach makes the carrier set of the lattice explicit, as e.g. in HOL/Algebra/Lattice.thy, the second one (in HOL/Lattices.thy and HOL/Lattices/*) uses implicit carrier sets (the UNIV-set of a type) and type-classes.

Is there a systematic/automatic way to go from theorems with the implicit carrier set to corresponding theorems for an explicit carrier set?

Clemens

**References**:

- Previous by Date: Re: [isabelle] Isabella proof general
- Next by Date: [isabelle] Simplifier problem (Congruence rules?)
- Previous by Thread: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set
- Next by Thread: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set[SEC=UNCLASSIFIED]
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list