@manual{isa-imp,
  author	= {Makarius Wenzel},
  title		= {The {Isabelle/Isar} Implementation},
  institution	= {Technische Universit\"at M\"unchen},
  note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}


@Book{isa-tutorial,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  year		= 2002,
  note		= {LNCS Tutorial 2283}}

@book{paulson-ml2,
  author	= {Lawrence C. Paulson},
  title		= {{ML} for the Working Programmer},
  year		= 1996,
  edition	= {2nd},
  publisher	= {Cambridge University Press}}