@manual{
  R1,
  author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
  title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
  month=nov,
  year=2013,
  note={\url{http://isabelle.in.tum.de/website-Isabelle2013-1/dist/Isabelle2013-1/doc/tutorial.pdf}}
}

@manual{
  R2,
  author={Tobias Nipkow},
  title="Programming and Proving in Isabelle/HOL",
  month=nov,
  year=2013,
  note={\url{http://isabelle.in.tum.de/website-Isabelle2013-1/dist/Isabelle2013-1/doc/prog-prove.pdf}}
}

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

@manual{
  R4,
  author={Alexander Krauss},
  title="Defining Recursive Functions in Isabelle/HOL",
  note={\url{http://isabelle.in.tum.de/website-Isabelle2013-1/dist/Isabelle2013-1/doc/functions.pdf}}
}

@misc{
  R5,
  title="Isabelle/HOL Exercises --- Advanced --- Sorting with Lists and Trees",
  note={\url{http://isabelle.in.tum.de/exercises/advanced/sorting/ex.pdf}}
}
