src/HOL/Examples/document/root.bib

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/document/root.bib	Mon Jun 08 21:38:41 2020 +0200
@@ -0,0 +1,114 @@
+
+@string{CUCL="Comp. Lab., Univ. Camb."}
+@string{CUP="Cambridge University Press"}
+@string{Springer="Springer-Verlag"}
+@string{TUM="TU Munich"}
+
+@article{church40,
+  author	= "Alonzo Church",
+  title		= "A Formulation of the Simple Theory of Types",
+  journal	= "Journal of Symbolic Logic",
+  year		= 1940,
+  volume	= 5,
+  pages		= "56-68"}
+
+@Book{Concrete-Math,
+  author = 	 {R. L. Graham and D. E. Knuth and O. Patashnik},
+  title = 	 {Concrete Mathematics},
+  publisher = 	 {Addison-Wesley},
+  year = 	 1989
+}
+
+@InProceedings{Naraschewski-Wenzel:1998:HOOL,
+  author	= {Wolfgang Naraschewski and Markus Wenzel},
+  title		= {Object-Oriented Verification based on Record Subtyping in
+                  {H}igher-{O}rder {L}ogic},
+  crossref      = {tphols98}}
+
+@Article{Nipkow:1998:Winskel,
+  author = 	 {Tobias Nipkow},
+  title = 	 {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
+  journal = 	 {Formal Aspects of Computing},
+  year = 	 1998,
+  volume =	 10,
+  pages =	 {171--186}
+}
+
+@InProceedings{Wenzel:1999:TPHOL,
+  author = 	 {Markus Wenzel},
+  title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+  crossref =     {tphols99}}
+
+@Book{Winskel:1993,
+  author = 	 {G. Winskel},
+  title = 	 {The Formal Semantics of Programming Languages},
+  publisher = 	 {MIT Press},
+  year = 	 1993
+}
+
+@Book{davey-priestley,
+  author	= {B. A. Davey and H. A. Priestley},
+  title		= {Introduction to Lattices and Order},
+  publisher	= CUP,
+  year		= 1990}
+
+@TechReport{Gordon:1985:HOL,
+  author =       {M. J. C. Gordon},
+  title =        {{HOL}: A machine oriented formulation of higher order logic},
+  institution =  {University of Cambridge Computer Laboratory},
+  year =         1985,
+  number =       68
+}
+
+@manual{isabelle-HOL,
+  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+  title		= {{Isabelle}'s Logics: {HOL}},
+  institution	= {Institut f\"ur Informatik, Technische Universi\"at
+                  M\"unchen and Computer Laboratory, University of Cambridge}}
+
+@manual{isabelle-intro,
+  author	= {Lawrence C. Paulson},
+  title		= {Introduction to {Isabelle}},
+  institution	= CUCL}
+
+@manual{isabelle-isar-ref,
+  author	= {Markus Wenzel},
+  title		= {The {Isabelle/Isar} Reference Manual},
+  institution	= TUM}
+
+@manual{isabelle-ref,
+  author	= {Lawrence C. Paulson},
+  title		= {The {Isabelle} Reference Manual},
+  institution	= CUCL}
+
+@Book{paulson-isa-book,
+  author	= {Lawrence C. Paulson},
+  title		= {Isabelle: A Generic Theorem Prover},
+  publisher	= {Springer},
+  year		= 1994,
+  note		= {LNCS 828}}
+
+@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.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}}
+}
+
+@Proceedings{tphols98,
+  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
+  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
+  editor	= {Jim Grundy and Malcom Newey},
+  series	= {LNCS},
+  volume        = 1479,
+  year		= 1998}
+
+@Proceedings{tphols99,
+  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+  editor	= {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
+                  Paulin, C. and Thery, L.},
+  series	= {LNCS 1690},
+  year		= 1999}