# From LCF to Isabelle/HOL

## TL;DR

This paper reviews the development of Isabelle/HOL, highlighting its unique features like automatic proof search, counterexample finding, and a user-friendly environment, demonstrating its evolution from early LCF systems to a practical theorem proving tool.

## Contribution

It provides a comprehensive overview of Isabelle/HOL's features and its progression from foundational LCF concepts to a versatile, user-friendly theorem prover.

## Key findings

- Isabelle/HOL integrates automatic proof search and counterexample generation.
- It offers a structured, readable proof language and interactive environment.
- Isabelle/HOL is widely used across various scientific and engineering fields.

## Abstract

Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing techniques from the world of first order theorem proving, but also the automatic search for counterexamples. They include a highly readable structured language of proofs and a unique interactive development environment for editing live proof documents. Everything rests on the foundation conceived by Robin Milner for Edinburgh LCF: a proof kernel, using abstract types to ensure soundness and eliminate the need to store proofs. Compared with the research prototypes of the 1970s, Isabelle is a practical and versatile tool. It is used by system designers, mathematicians and many others.