*To*: Benedikt.AHRENS at unice.fr*Subject*: Re: [isabelle] locales & category theory*From*: Makarius <makarius at sketis.net>*Date*: Fri, 17 Apr 2009 13:58:41 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <49E75DE7.4020309@unice.fr>*References*: <49E75DE7.4020309@unice.fr>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Thu, 16 Apr 2009, Benedikt.AHRENS at unice.fr wrote:

What does the keyword "structure" in parentheses in the following codeexcerpt mean? I looked for it in the Isabelle tutorial (which does notcover locales, unfortunately) as well as in "Locales - a sectioningconcept..." but could not find it.

locale category = fixes CC (structure) assumes dom_object [intro]: "f : Ar ==> Dom f : Ob"

Makarius

**References**:**[isabelle] locales & category theory***From:*Benedikt . AHRENS

- Previous by Date: Re: [isabelle] Obtaining the instantiation of variables in a proof
- Next by Date: [isabelle] installing isa2009-test
- Previous by Thread: [isabelle] locales & category theory
- Next by Thread: [isabelle] installing isa2009-test
- Cl-isabelle-users April 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