src/HOL/Isar_examples/document/root.bib
changeset 7968 964b65b4e433
parent 7816 2840e8857523
child 7977 67bfcd3a433c
--- 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},