Editing Isabelle (proof assistant) (section)

{{Short description|Higher-order logic (HOL) automated theorem prover}}
{{Infobox software
| name = Isabelle
| logo = 
| screenshot = Isabelle jedit.png
| caption = Isabelle–jEdit running on [[macOS]] 
| author = [[Lawrence Paulson]]
| developer = [[University of Cambridge]]<br/>[[Technical University of Munich]], et al.
| released = {{Start date and age|1986}}<ref>{{Cite journal |last1=Paulson |first1=L. C. |author1-link=Lawrence Paulson |year=1986 |title=Natural deduction as higher-order resolution |journal=The Journal of Logic Programming |volume=3 |issue=3 |pages=237–258 |doi=10.1016/0743-1066(86)90015-4 |arxiv=cs/9301104 |s2cid=27085090}}</ref>
| latest release version=Isabelle2025
| latest release date = {{Start date and age|2025|03}}
| programming language = [[Standard ML]], [[Scala (programming language)|Scala]]
| operating system = [[Linux]], [[Windows]], [[macOS]]
| genre = [[Mathematics]]
| license = [[BSD licenses|BSD]]
| website = {{URL|isabelle.in.tum.de}}
}}

The '''Isabelle'''{{efn|{{IPAc-en|ˌ|ɪ|z|ə|ˈ|b|ɛ|l}}}} [[automated theorem prover]] is a [[HOL (proof assistant)|higher-order logic (HOL) theorem prover]], written in [[Standard ML]] and [[Scala (programming language)|Scala]]. As a [[Logic for Computable Functions]] (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.

Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories and implementations for code-generating, documenting, and specific support for a variety of [[formal methods]]. It can be seen as an [[integrated development environment]] (IDE) for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle ''Archive of Formal Proofs'' ('''Isabelle AFP''').<ref>{{cite web |last1=Eberl |first1=Manuel |last2=Klein |first2=Gerwin |last3=Nipkow |first3=Tobias |last4=Paulson |first4=Larry |author4-link=Lawrence Paulson |last5=Thiemann |first5=René |title=Archive of Formal Proofs |url=https://www.isa-afp.org/ |access-date=1 May 2021 |ref=AFP}}</ref>

Isabelle was named by [[Lawrence Paulson]] after [[Gérard Huet]]'s daughter.<ref>{{cite web|url=http://www.cl.cam.ac.uk/~mjcg/Research94/node3.html|title=1.2 History|work=Isabelle and HOL|publisher=Cambridge AR Research (The Automated Reasoning Group)|last=Gordon|first=Mike|date=1994-11-16|access-date=2016-04-28|archive-date=2017-03-05|archive-url=https://web.archive.org/web/20170305020417/http://www.cl.cam.ac.uk/~mjcg/Research94/node3.html|url-status=dead}}</ref>

The Isabelle theorem prover is [[free software]], released under the revised [[BSD license]].