[isabelle] locales & category theory



Hello,

I am an Isabelle beginner and interested in the development on category theory on
http://afp.sourceforge.net/browser_info/devel/HOL/Category/
.
My long term goal is to extend this library a bit.

The code is more or less self-explaining, but I have one question:

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

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

When you answer, please put me in CC, since I haven't subscribed to the list yet.

Thanks a lot in advance,
ben





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.