--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/document/root.bib Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,48 @@
+
+@InProceedings{Bauer-Wenzel:2000:HB,
+ author = {Gertrud Bauer and Markus Wenzel},
+ title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
+ {I}sabelle/{I}sar},
+ booktitle = {Types for Proofs and Programs: TYPES'99},
+ editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
+ and Jan Smith},
+ series = {LNCS},
+ year = 2000
+}
+
+@Book{Davey-Priestley:1990,
+ author = {B. A. Davey and H. A. Priestley},
+ title = {Introduction to Lattices and Order},
+ publisher = {Cambridge University Press},
+ year = 1990}
+
+@InProceedings{Wenzel:1999:TPHOL,
+ author = {Markus Wenzel},
+ title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+ crossref = {tphols99}}
+
+
+@Manual{Wenzel:2000:axclass,
+ author = {Markus Wenzel},
+ title = {Using Axiomatic Type Classes in Isabelle},
+ year = 2000,
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}
+}
+
+@Manual{Wenzel:2000:isar-ref,
+ author = {Markus Wenzel},
+ title = {The {Isabelle/Isar} Reference Manual},
+ year = 2000,
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
+}
+
+@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},
+ volume = 1690,
+ year = 1999}