src/ZF/Constructible/document/root.bib

make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;

@incollection{goedel40,
  author	= {Kurt G\"odel},
  title		= {The Consistency of the Axiom of Choice and of the
		   Generalized Continuum Hypothesis with the Axioms of Set
		   Theory},
  booktitle	= {{Kurt G\"odel}: Collected Works},
  volume	= {II},
  editor	= {S. Feferman and others},
  publisher	= {Oxford University Press},
  year		= 1990},
  pages		= {33-101},
  note		= {First published in 1940 by Princeton University Press}}

@Book{kunen80,
  author	= {Kenneth Kunen},
  title		= {Set Theory: An Introduction to Independence Proofs},
  publisher	= "North-Holland",
  year		= 1980}

@ARTICLE{paulson-consistency,
  author = {Lawrence C. Paulson},
  title = {The Relative Consistency of the Axiom of Choice --- Mechanized Using {Isabelle/ZF}},
  journal = {LMS Journal of Computation and Mathematics},
  year = {2003},
  volume = {6},
  pages = {198-248},
  note = {\url{http://www.lms.ac.uk/jcm/6/lms2003-001/}},
}

@INPROCEEDINGS{paulson-reflection,
  author = {Lawrence C. Paulson},
  title = {The Reflection Theorem: A Study in Meta-Theoretic Reasoning},
  pages = {377-391},
  editor	= {Andrei Voronkov},
  booktitle	= {Automated Deduction --- {CADE}-18 
		  International Conference},
  year		= 2002,
  series	= {LNAI 2392},
  publisher	= {Springer}}
}