--- a/src/HOL/ex/document/root.bib Fri Apr 21 21:06:02 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-@inproceedings{HuttonW04,author={Graham Hutton and Joel Wright},
-title={Compiling Exceptions Correctly},
-booktitle={Proc.\ Conf.\ Mathematics of Program Construction},
-year=2004,note={To appear}}
-
-@InProceedings{Kamm-et-al:1999,
- author = {Florian Kamm{\"u}ller and Markus Wenzel and
- Lawrence C. Paulson},
- title = {Locales: A Sectioning Concept for {Isabelle}},
- 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},
- volume = 1690,
- year = 1999}
-
-@InProceedings{Naraschewski-Wenzel:1998,
- author = {Wolfgang Naraschewski and Markus Wenzel},
- title = {Object-Oriented Verification based on Record Subtyping in
- {H}igher-{O}rder {L}ogic},
- booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
- editor = {Jim Grundy and Malcom Newey},
- series = {LNCS},
- volume = 1479,
- year = 1998}
-
-@Manual{Nipkow-et-al:2001:HOL,
- author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
- title = {{Isabelle}'s Logics: {HOL}},
- institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
- M{\"u}nchen and Computer Laboratory, University of Cambridge},
- year = 2001,
- note = {Part of the Isabelle distribution,
- \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
-}
-
-@Article{Paulson:1989,
- author = {L. C. Paulson},
- title = {The foundation of a generic Theorem Prover},
- journal = {Journal of Automated Reasoning},
- year = 1989,
- volume = 5,
- number = 3,
- pages = {363--397}
-}
-
-@Book{Paulson:1994:Isabelle,
- author = {L. C. Paulson and T. Nipkow},
- title = {{Isabelle}: A Generic Theorem Prover},
- year = 1994,
- series = {LNCS},
- volume = {828},
- publisher = {Springer}
-}
-
-@InProceedings{Wenzel:1999,
- author = {Markus Wenzel},
- title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
- 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},
- volume = 1690,
- year = 1999}
-
-@Unpublished{Wenzel:2001:Isar-examples,
- author = {Markus Wenzel},
- title = {Miscellaneous {I}sabelle/{I}sar examples for
- Higher-Order Logic},
- year = 2001,
- note = {Part of the Isabelle distribution,
- \url{http://isabelle.in.tum.de/library/HOL/Isar_Examples/document.pdf}}
-}
-
-@PhdThesis{Wenzel:2001:Thesis,
- author = {Markus Wenzel},
- title = {Isabelle/Isar --- a versatile environment for human-readable
- formal proof documents},
- school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
- year = 2001,
- month = {September},
- note = {Submitted}
-}
-@Manual{Wenzel:2001:isar-ref,
- author = {Markus Wenzel},
- title = {The {Isabelle/Isar} Reference Manual},
- year = 2001,
- institution = {TU M{\"u}nchen},
- note = {Part of the Isabelle distribution,
- \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
-}
-
-@Book{isabelle-hol-book,
- author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
- title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
- publisher = {Springer},
- year = 2002,
- note = {LNCS 2283}}
-
-@Misc{McMillan-LectureNotes,
- author = {Ken McMillan},
- title = {Lecture notes on verification of digital and hybrid systems},
- note = {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
-}
-
-@PhdThesis{McMillan-PhDThesis,
- author = {Ken McMillan},
- title = {Symbolic Model Checking: an approach to the state explosion problem},
- school = {Carnegie Mellon University},
- year = 1992
-}
\ No newline at end of file