--- a/src/HOL/Isar_examples/document/root.bib Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/document/root.bib Thu Oct 28 19:57:34 1999 +0200
@@ -5,6 +5,11 @@
@string{TUM="TU Munich"}
+@InProceedings{Wenzel:1999:TPHOL,
+ author = {Markus Wenzel},
+ title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+ crossref = {tphols99}}
+
@Book{davey-priestley,
author = {B. A. Davey and H. A. Priestley},
title = {Introduction to Lattices and Order},
@@ -24,13 +29,22 @@
@manual{isabelle-isar-ref,
author = {Markus Wenzel},
- title = {The {Isabelle Isar} Reference Manual},
+ title = {The {Isabelle/Isar} Reference Manual},
institution = TUM}
-@InProceedings{Wenzel:1999:TPHOL,
- author = {Markus Wenzel},
- title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
- crossref = {tphols99}}
+@manual{isabelle-ref,
+ author = {Lawrence C. Paulson},
+ title = {The {Isabelle} Reference Manual},
+ institution = CUCL}
+
+@TechReport{paulson-mutilated-board,
+ author = {Lawrence C. Paulson},
+ title = {A Simple Formalization and Proof for the Mutilated Chess Board},
+ institution = CUCL,
+ year = 1996,
+ number = 394,
+ note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.pdf}}
+}
@Proceedings{tphols99,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},