@Proceedings{TPHOLS99,
  title =   {Theorem Proving in Higher Order Logics},
  year =   1999,
  editor =  {Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry},
  volume =  1690,
  series =  {Lecture Notes in Computer Science},
  address =  {\href{URL}{\url{http://link.springer.de/link/service/series/0558/tocs/t1690.htm}}},
  month =  {September},
  publisher =  {Springer}
}

@InProceedings{Wen99,
  author =   {Markus Wenzel},
  title =   {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
  booktitle =  {Theorem Proving in Higher Order Logics},
  note = {\cite{TPHOLS99}}
}


@InProceedings{Kam99,
  author =   {Florien Kamm\"{u}ller and Markus Wenzel and Lawrence C. Paulson},
  title =   {Locales: A Sectioning Concept for {I}sabelle},
  booktitle =  {Theorem Proving in Higher Order Logics},
  year =  1999,
  note =  {\cite{TPHOLS99}}
}


@InProceedings{fcat4cats,
  author =   {Greg O'Keefe},
  year =   2004,
  title =   {Towards a Readable Formalisation of Category Theory},
  booktitle =   {Computing: The Australasian Theory Symposium},
  editor =  {Mike Atkinson},
  volume =  91,
  pages =        {212-228},
  series =  {Electronic Notes in Theoretical Computer Science},
  publisher =  {Elsevier}
}