Papers about Isabelle

• L. C. Paulson.
  The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397. Publisher's version
• L. C. Paulson.
  Isabelle: the next 700 theorem provers. In: P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361–386.
• L. C. Paulson.
  Tool support for logics of programs. In: M. Broy (editor), Mathematical Methods in Program Development (Summer School Marktoberdorf 1996), Springer-Verlag, 461–498. Also Report 406, Computer Lab (1996). Slides available
• Strategic principles in the design of Isabelle.
  CADE-15 Workshop on Strategies in Automated Deduction, Lindau, Germany (1998), 11–17.
  Slides available

• J. Fleuriot and L. C. Paulson.
  Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. In: Xiao-Shan Gao, Dongming Wang and Lu Yang (editors), Automated Deduction in Geometry, Second International Workshop, ADG '98 (Springer LNCS 1669, published 1999), 47–66.
• F. Kammüller and L. C. Paulson.
  A formal proof of Sylow's theorem: An experiment in abstract algebra with Isabelle HOL. J. Automated Reasoning 23 (1999), 235–264.
• L. C. Paulson.
  The relative consistency of the axiom of choice mechanized using Isabelle/ZF.
  LMS J. Computation and Mathematics 6 (2003), 198–248.
  Slides and theory document available
• L. C. Paulson.
  Organizing Numerical Theories Using Axiomatic Type Classes. Journal of Automated Reasoning 33 1 (2004), 29–49. Slides available
• L. C. Paulson.
  Defining Functions on Equivalence Classes. ACM Trans. on Computational Logic 7 4 (2006), 658–675. Slides available

• L. C. Paulson,
  Generic automatic proof tools. In: Robert Veroff (editor), Automated Reasoning and its Applications: Essays in Honor of Larry Wos (MIT Press, 1997), 23–47.
• L. C. Paulson,
  A generic tableau prover and its integration with Isabelle.
  J. Universal Computer Science 5 (3) (1999), 73–87.

See also papers on linking Isabelle with automatic provers.

• L. C. Paulson,
  Natural deduction as higher-order resolution. J. Logic Programming 3 (1986), 237–258.
• L. C. Paulson,
  Isabelle: the next seven hundred theorem provers (system abstract). In: E. Lusk and R. Overbeek (editors), 9th International Conf. on Automated Deduction (Springer LNCS 310, 1988), 772–773.
• L. C. Paulson,
  A formulation of the simple theory of types (for Isabelle). In: P. Martin-Löf &G. Mints (editors), COLOG-88: International Conf. in Computer Logic.Tallinn, Estonia (1988). Published as Springer LNCS 417, 1990), 246–274.
• L. C. Paulson.
  A preliminary user's manual for Isabelle. Technical Report 133, Computer Lab (1988).
• Tobias Nipkow and L C Paulson,
  Isabelle tutorial and user's manual. Technical Report 189, Computer Lab (1990).
• L. C. Paulson,
  Introduction to Isabelle. Technical Report, Computer Lab (last revised 2003).