src/HOL/Library/document/root.bib

proper option;

@Unpublished{Abrial-Laffitte,
  author = 	 {Abrial and Laffitte},
  title = 	 {Towards the Mechanization of the Proofs of
                  Some Classical Theorems of Set Theory},
  note = 	 {Unpublished}
}

@Book{Oberschelp:1993,
  author =	 {Arnold Oberschelp},
  title = 	 {Rekursionstheorie},
  publisher = 	 {BI-Wissenschafts-Verlag},
  year = 	 1993
}

@InProceedings{Podelski-Rybalchenko,
  author = 	 {Andreas Podelski and Andrey Rybalchenko},
  title = 	 {Transition Invariants},
  booktitle = 	 {19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)},
  pages =	 {32--41},
  year =	 2004
}

@Book{davenport92,
  author =	 {H. Davenport},
  title = 	 {The Higher Arithmetic},
  publisher = 	 {Cambridge University Press},
  year = 	 1992
}

@InProceedings{paulin-tlca,
  author	= {Christine Paulin-Mohring},
  title		= {Inductive Definitions in the System {Coq}: Rules and
		 Properties},
  crossref	= {tlca93},
  pages		= {328-345}}

@Proceedings{tlca93,
  title		= {Typed Lambda Calculi and Applications},
  booktitle	= {Typed Lambda Calculi and Applications},
  editor	= {M. Bezem and J.F. Groote},
  year		= 1993,
  publisher	= {Springer},
  series	= {LNCS 664}}

@article{leijen01,
  author  = {Leijen, Daan},
  title   = {Division and Modulus for Computer Scientists},
  year    = 2001,
  url     = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf}}

@InProceedings{LochbihlerStoop2018,
  author = {Andreas Lochbihler and Pascal Stoop},
  title = {Lazy Algebraic Types in {Isabelle/HOL}},
  booktitle = {Isabelle Workshop 2018},
  year = 2018,
}

@inproceedings{Haftmann-Nipkow:2010:code,
  author =      {Florian Haftmann and Tobias Nipkow},
  title =       {Code Generation via Higher-Order Rewrite Systems},
  booktitle =   {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
  year =        2010,
  publisher =   Springer,
  series =      LNCS,
  editor =      {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
  volume =      6009
}