@book{
  Nipkow14,
  author = {Tobias Nipkow and Gerwin Klein},
  title = {Concrete Semantics with Isabelle/HOL},
  month = mar,
  year = 2021,
  publisher = {Springer-Verlag},
  note = {(Current version: \url{http://www.concrete-semantics.org/concrete-semantics.pdf})}
}

@misc{
  Klein21,
  author = {Gerwin Klein},
  title = {{Theory HOL-IMP.Compiler2 (included in the Isabelle2021 distribution)}},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2021/dist/library/HOL/HOL-IMP/Compiler2.html}}
}

@manual{
  Paulson21,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title = {Isabelle/HOL -- A Proof Assistant for Higher-Order Logic},
  month = feb,
  year = 2021,
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021/doc/tutorial.pdf}}
}

@manual{
  Nipkow21,
  author = {Tobias Nipkow},
  title = {Programming and Proving in Isabelle/HOL},
  month = feb,
  year = 2021,
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021/doc/prog-prove.pdf}}
}

@manual{
  Krauss21,
  author = {Alexander Krauss},
  title = {Defining Recursive Functions in Isabelle/HOL},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021/doc/functions.pdf}}
}

@manual{
  Nipkow11,
  author = {Tobias Nipkow},
  title = {A Tutorial Introduction to Structured Isar Proofs},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/isar-overview.pdf}}
}
