HOL: Higher-Order Logic

These are the main sources of the Isabelle system for Higher-Order Logic.

There are also several example sessions:

Algebra
rings and univariate polynomials
Auth
a new approach to verifying authentication protocols
AxClasses
a few basic examples of using axiomatic type classes
Complex
a development of the complex numbers, the reals, and the hyper-reals, which are used in non-standard analysis (builds the image HOL-Complex)
Hoare
verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants)
HoareParallel
verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically)
Hyperreal
Nonstandard analysis. Builds on Real and is part of Complex.
IMP
mechanization of a large part of a semantics text by Glynn Winskel
IMPP
extension of IMP with local variables and mutually recursive procedures
Import
theories imported from other (HOL) theorem provers.
Induct
examples of (co)inductive definitions
IOA
a simple theory of Input/Output Automata
Isar_Examples
several introductory examples using Isabelle/Isar
Lambda
fundamental properties of lambda-calculus (Church-Rosser and termination)
Lattice
lattices and order structures (in Isabelle/Isar)
Library
A collection of generic theories
Matrix
two-dimensional matrices
MicroJava
formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety
Modelcheck
basic setup for integration of some model checkers in Isabelle/HOL
NanoJava
Haore Logic for a tiny fragment of Java
NumberTheory
fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
Prolog
a (bare-bones) implementation of Lambda-Prolog
Real
the real numbers, part of Complex
Hahn_Banach
the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
SET_Protocol
verification of the SET Protocol
Subst
a theory of substitution and unification.
TLA
Lamport's Temporal Logic of Actions (with separate example sessions)
UNITY
Chandy and Misra's UNITY formalism
W0
a precursor of MiniML, without let-expressions
ex
miscellaneous examples