---
title: "Isabelle: The Next 700 Theorem Provers (1990)"
description: "The central design choice is to write inference rules literally, as premises plus a conclusion. 25 references, cited by 6 papers here."
authors: ["Lawrence C. Paulson"]
year: 1990
venue: "arXiv:cs/9301106 (published in P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361-386)"
source: "https://arxiv.org/abs/cs/9301106"
doi: "10.48550/arxiv.cs/9301106"
arxiv: "cs/9301106"
licence: "arXiv — no licence stated; read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [1990](https://md.research.elamur.ai/free/en/papers/1990/) / Isabelle: The Next 700 Theorem Provers

# Isabelle: The Next 700 Theorem Provers

**Authors:** [Lawrence C. Paulson](https://md.research.elamur.ai/free/en/authors/lawrence-c-paulson/) · **Year:** 1990 · **Venue:** arXiv:cs/9301106 (published in P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361-386) · **Licence:** arXiv — no licence stated; read only

**Links:** [Publisher's page](https://arxiv.org/abs/cs/9301106) · [PDF](https://arxiv.org/pdf/cs/9301106v1) · [DOI 10.48550/arxiv.cs/9301106](https://doi.org/10.48550/arxiv.cs/9301106) · [arXiv cs/9301106](https://arxiv.org/abs/cs/9301106) · [OpenAlex](https://openalex.org/W4394639621)

**Citations:** 34 citations (OpenAlex, 2026-10-14) · [6](https://md.research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper surveys Isabelle, a generic interactive theorem prover. Rather than building a separate LCF-style system for each new logic, Isabelle tackles problems common to all logics once, so that each logic only needs its own specific parts. Paulson tells the system's history, starting from Milner's Edinburgh LCF with its tactics and tacticals, and frankly records the mistakes made along the way.

The central design choice is to write inference rules literally, as premises plus a conclusion. Proofs are then built by joining rules through Huet's higher-order unification. The early system, Isabelle-86, was later replaced by a meta-logic with implication, a universal quantifier and equality. This meta-logic handles assumption discharge, eigenvariables, natural deduction and derived rules cleanly. A comparison is drawn between this method and the Logical Framework developed at Edinburgh.

Several object-logics are presented, including Constructive Type Theory, first-order logics and Zermelo-Fraenkel set theory. The paper matters because it shows one small, generic kernel can support many formal theories with reasonable automation. It also argues that powerful tools remain more important than a friendly interface.

## Key points
- Isabelle is written entirely in Standard ML. Its core technique is higher-order unification (Huet, 1975), which is undecidable in theory but proved reliable in practice.
- In Isabelle-86, repeated rule application in the sequent calculus automatically solved roughly 35 of Pelletier's (1986) problems. Sequence variables were obtained by encoding lists so that unification behaves associatively.
- Early versions were very slow. Removing Skolem terms and replacing structure sharing with copying made the system both simpler and faster.
- The newer meta-logic is a fragment of higher-order logic built from implication (⟹), universal quantification (⋀) and equality (≡).
- The Zermelo-Fraenkel set theory development includes about 60 examples, such as the justification of the pairing definition ⟨a,b⟩ = {{a},{a,b}}. Users extended the system further: Noël developed fixedpoint theory, and Nipkow (1989) built rewriting tactics.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [École Polytechnique Fédérale de Lausanne](https://md.research.elamur.ai/free/en/universities/ecole-polytechnique-federale-de-lausanne/) — University, Lausanne, Switzerland · 56 works · 8,189 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Lawrence C. Paulson. 1990. Isabelle: The Next 700 Theorem Provers. arXiv:cs/9301106 (published in P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361-386).

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{paulson1990isabelle,
  title = {{Isabelle: The Next 700 Theorem Provers}},
  author = {Lawrence C. Paulson},
  year = {1990},
  doi = {10.48550/arxiv.cs/9301106},
  eprint = {cs/9301106},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.cs/9301106}
}
```

- [← previous A Multi-Level Account of Cleft Constructions in Discourse](https://md.research.elamur.ai/free/en/papers/delin-1990-multi-level-account-cleft-constructions/)
- [next → Reversible Unification Based Machine Translation](https://md.research.elamur.ai/free/en/papers/noord-1990-reversible-unification-based-machine-translation/)
- [↑ back to papers of 1990](https://md.research.elamur.ai/free/en/papers/1990/)

## References

25 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Peter B. Andrews, Dale A. Miller, Eve L. Cohen, and Frank Pfenning (1984). Automating higher-order logic. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 169–192, American Mathematical Society. [find](https://scholar.google.com/scholar?q=Peter+B%2E+Andrews%2C+Dale+A%2E+Miller%2C+Eve+L%2E+Cohen%2C+and+Frank+Pfenning+%281984%29%2E+Automating+higher%2Dorder+logic%2E+In+W%2E+W%2E+Bledsoe+and+D%2E+W%2E+Loveland%2C+editors%2C+Automated+Theorem+Proving%3A+After+25+Years%2C+pages)
2. Peter B. Andrews (1986). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press. [find](https://scholar.google.com/scholar?q=Peter+B%2E+Andrews+%281986%29%2E+An+Introduction+to+Mathematical+Logic+and+Type+Theory%3A+To+Truth+Through+Proof%2E+Academic+Press%2E)
3. A. Avron, F. A. Honsell, and I. A. Mason (1987). Using typed lambda calculus to implement formal systems on a machine. Report ecs-lfcs-87-31. Computer Science Department, University of Edinburgh. [find](https://scholar.google.com/scholar?q=A%2E+Avron%2C+F%2E+A%2E+Honsell%2C+and+I%2E+A%2E+Mason+%281987%29%2E+Using+typed+lambda+calculus+to+implement+formal+systems+on+a+machine%2E+Report+ecs%2Dlfcs%2D87%2D31%2E+Computer+Science+Department%2C+University+of+Edinburgh%2E)
4. Graham Birtwistle and P. A. Subrahmanyam (1988), editors. VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers. [find](https://scholar.google.com/scholar?q=Graham+Birtwistle+and+P%2E+A%2E+Subrahmanyam+%281988%29%2C+editors%2E+VLSI+Specification%2C+Verification+and+Synthesis%2E+Kluwer+Academic+Publishers%2E)
5. Alonzo Church (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68. [find](https://scholar.google.com/scholar?q=Alonzo+Church+%281940%29%2E+A+formulation+of+the+simple+theory+of+types%2E+Journal+of+Symbolic+Logic%2C+5%3A56%E2%80%9368%2E)
6. R. L. Constable et al. (1986). Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall International. [find](https://scholar.google.com/scholar?q=R%2E+L%2E+Constable+et+al%2E+%281986%29%2E+Implementing+Mathematics+with+the+Nuprl+Proof+Development+System%2E+Prentice%2DHall+International%2E)
7. N. G. de Bruijn (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indagationes Mathematicae, 34:381–392. [find](https://scholar.google.com/scholar?q=N%2E+G%2E+de+Bruijn+%281972%29%2E+Lambda+calculus+notation+with+nameless+dummies%2C+a+tool+for+automatic+formula+manipulation%2C+with+application+to+the+Church%2DRosser+Theorem%2E+Indagationes+Mathematicae%2C+34%3A381%E2%80%93392%2E)
8. Amy Felty and Dale Miller (1988). Specifying theorem provers in a higher-order logic programming language. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, pages 61–80, Springer-Verlag. LNCS 310. [find](https://scholar.google.com/scholar?q=Amy+Felty+and+Dale+Miller+%281988%29%2E+Specifying+theorem+provers+in+a+higher%2Dorder+logic+programming+language%2E+In+E%2E+Lusk+and+R%2E+Overbeek%2C+editors%2C+9th+International+Conference+on+Automated+Deduction%2C+pag)
9. Michael J. C. Gordon (1988). HOL: a proof generating system for higher-order logic. In Birtwistle and Subrahmanyam (1988), pages 73–128. [find](https://scholar.google.com/scholar?q=Michael+J%2E+C%2E+Gordon+%281988%29%2E+HOL%3A+a+proof+generating+system+for+higher%2Dorder+logic%2E+In+Birtwistle+and+Subrahmanyam+%281988%29%2C+pages+73%E2%80%93128%2E)
10. R. Harper, F. Honsell and G. Plotkin (1987). A Framework for Defining Logics. Symposium on Logic in Computer Science. ieee Computer Society Press, 194–204. [find](https://scholar.google.com/scholar?q=R%2E+Harper%2C+F%2E+Honsell+and+G%2E+Plotkin+%281987%29%2E+A+Framework+for+Defining+Logics%2E+Symposium+on+Logic+in+Computer+Science%2E+ieee+Computer+Society+Press%2C+194%E2%80%93204%2E)
11. G. P. Huet (1975). A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57. [find](https://scholar.google.com/scholar?q=G%2E+P%2E+Huet+%281975%29%2E+A+unification+algorithm+for+typed+%CE%BB%2Dcalculus%2E+Theoretical+Computer+Science%2C+1%3A27%E2%80%9357%2E)
12. G. P. Huet and B. Lang (1978). Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31–55. [find](https://scholar.google.com/scholar?q=G%2E+P%2E+Huet+and+B%2E+Lang+%281978%29%2E+Proving+and+applying+program+transformations+expressed+with+second%2Dorder+patterns%2E+Acta+Informatica%2C+11%3A31%E2%80%9355%2E)
13. Per Martin-Löf (1984). Intuitionistic type theory. Bibliopolis. [find](https://scholar.google.com/scholar?q=Per+Martin%2DLo%CC%88f+%281984%29%2E+Intuitionistic+type+theory%2E+Bibliopolis%2E)
14. Tobias Nipkow (1989). Equational reasoning in Isabelle. Science of Computer Programming, 12:123–149. [find](https://scholar.google.com/scholar?q=Tobias+Nipkow+%281989%29%2E+Equational+reasoning+in+Isabelle%2E+Science+of+Computer+Programming%2C+12%3A123%E2%80%93149%2E)
15. B. Nordström and J. M. Smith (1984). Propositions and specifications of programs in Martin-Löf’s type theory. BIT, 24:288–301. [find](https://scholar.google.com/scholar?q=B%2E+Nordstro%CC%88m+and+J%2E+M%2E+Smith+%281984%29%2E+Propositions+and+specifications+of+programs+in+Martin%2DLo%CC%88f%E2%80%99s+type+theory%2E+BIT%2C+24%3A288%E2%80%93301%2E)
16. L. C. Paulson (1986). Natural deduction as higher-order resolution. Journal of Logic Programming, 3:237–258. [find](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson+%281986%29%2E+Natural+deduction+as+higher%2Dorder+resolution%2E+Journal+of+Logic+Programming%2C+3%3A237%E2%80%93258%2E)
17. L. C. Paulson (1987). Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press. [find](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson+%281987%29%2E+Logic+and+Computation%3A+Interactive+proof+with+Cambridge+LCF%2E+Cambridge+University+Press%2E)
18. L. C. Paulson (1988). A preliminary user’s manual for Isabelle. Technical Report 133, University of Cambridge Computer Laboratory. [find](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson+%281988%29%2E+A+preliminary+user%E2%80%99s+manual+for+Isabelle%2E+Technical+Report+133%2C+University+of+Cambridge+Computer+Laboratory%2E)
19. L. C. Paulson (1989). The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397. [find](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson+%281989%29%2E+The+foundation+of+a+generic+theorem+prover%2E+Journal+of+Automated+Reasoning%2C+5%3A363%E2%80%93397%2E)
20. F. J. Pelletier (1986). Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216. Errata, JAR 4 (1988), 236–236. [find](https://scholar.google.com/scholar?q=F%2E+J%2E+Pelletier+%281986%29%2E+Seventy%2Dfive+problems+for+testing+automatic+theorem+provers%2E+Journal+of+Automated+Reasoning%2C+2%3A191%E2%80%93216%2E+Errata%2C+JAR+4+%281988%29%2C+236%E2%80%93236%2E)
21. D. Prawitz (1965). Natural Deduction: A Proof-theoretical Study. Almquist and Wiksell. [find](https://scholar.google.com/scholar?q=D%2E+Prawitz+%281965%29%2E+Natural+Deduction%3A+A+Proof%2Dtheoretical+Study%2E+Almquist+and+Wiksell%2E)
22. P. Schroeder-Heister (1984). Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ∨, ⊃, ⊥, ∀, ∃. In Computation and Proof Theory: Logic Colloquium ’83, pages 399–426, Springer-Verlag. Lecture Notes in Mathematics 1104. [find](https://scholar.google.com/scholar?q=P%2E+Schroeder%2DHeister+%281984%29%2E+Generalized+rules+for+quantifiers+and+the+completeness+of+the+intuitionistic+operators+%26%2C+%E2%88%A8%2C+%E2%8A%83%2C+%E2%8A%A5%2C+%E2%88%80%2C+%E2%88%83%2E+In+Computation+and+Proof+Theory%3A+Logic+Colloquium+%E2%80%9983%2C+pages+399%E2%80%934)
23. Stefan SokoÃlowski (1987). Soundness of Hoare’s logic: an automatic proof using LCF. ACM Transactions on Programming Languages and Systems, 9:100–120. [find](https://scholar.google.com/scholar?q=Stefan+Soko%C3%83lowski+%281987%29%2E+Soundness+of+Hoare%E2%80%99s+logic%3A+an+automatic+proof+using+LCF%2E+ACM+Transactions+on+Programming+Languages+and+Systems%2C+9%3A100%E2%80%93120%2E)
24. G. Takeuti (1987). Proof Theory, 2nd edition. North Holland. [find](https://scholar.google.com/scholar?q=G%2E+Takeuti+%281987%29%2E+Proof+Theory%2C+2nd+edition%2E+North+Holland%2E)
25. Å. Wikström (1987). Functional Programming using ML. Prentice-Hall International. [find](https://scholar.google.com/scholar?q=A%CC%8A%2E+Wikstro%CC%88m+%281987%29%2E+Functional+Programming+using+ML%2E+Prentice%2DHall+International%2E)

*Updated 3 November 2026*