- HOL
Classical Higher-order Logic.

- HOL-Algebra
Author: Clemens Ballarin, started 24 September 1999 The Isabelle Algebraic Library.

- HOL-Auth
A new approach to verifying authentication protocols.

- HOL-BNF
Bounded Natural Functors for (Co)datatypes.

- HOL-BNF-Examples
Examples for Bounded Natural Functors.

- HOL-BNF-LFP
Bounded Natural Functors for Datatypes.

- HOL-BNF-Nitpick_Examples
Author: Jasmin Blanchette, TU Muenchen Copyright 2009

- HOL-Bali
- HOL-Cardinals
Ordinals and Cardinals, Full Theories.

- HOL-Cardinals-Base
Ordinals and Cardinals, Base Theories.

- HOL-Datatype_Benchmark
Some rather large datatype examples (from John Harrison).

- HOL-Decision_Procs
Various decision procedures, typically involving reflection.

- HOL-Hahn_Banach
Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace.

- HOL-Hoare
Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants).

- HOL-Hoare_Parallel
Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically).

- HOL-IMP
- HOL-IMPP
Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).

- HOL-IOA
Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz

- HOL-Imperative_HOL
- HOL-Import
- HOL-Induct
Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations.

- HOL-Isar_Examples
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.

- HOL-Lattice
Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders.

- HOL-Library
Classical Higher-order Logic -- batteries included.

- HOL-Matrix_LP
Two-dimensional matrices and linear programming.

- HOL-Metis_Examples
Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer.

- HOL-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.

- HOL-Mirabelle
- HOL-Mirabelle-ex
- HOL-Multivariate_Analysis
- HOL-Mutabelle
- HOL-NSA
Nonstandard analysis.

- HOL-NSA-Examples
- HOL-NanoJava
Hoare Logic for a tiny fragment of Java.

- HOL-Nominal
- HOL-Nominal-Examples
- HOL-Number_Theory
- HOL-Old_Number_Theory
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity.

- HOL-Predicate_Compile_Examples
- HOL-Probability
- HOL-Prolog
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system.

- HOL-Proofs
HOL-Main with explicit proof terms.

- HOL-Proofs-Extraction
Examples for program extraction in Higher-Order Logic.

- HOL-Proofs-Lambda
Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).

- HOL-Proofs-ex
- HOL-Quickcheck_Benchmark
- HOL-Quickcheck_Examples
- HOL-Quotient_Examples
Author: Cezary Kaliszyk and Christian Urban

- HOL-Record_Benchmark
Some benchmark on large record.

- HOL-SET_Protocol
Verification of the SET Protocol.

- HOL-SPARK
- HOL-SPARK-Examples
- HOL-SPARK-Manual
- HOL-Statespace
- HOL-TLA
Lamport's Temporal Logic of Actions.

- HOL-TLA-Buffer
- HOL-TLA-Inc
- HOL-TLA-Memory
- HOL-TPTP
Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions.

- HOL-UNITY
Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism.

- HOL-Unix
- HOL-Word
- HOL-Word-Examples
- HOL-Word-SMT_Examples
- HOL-ZF
- HOL-ex
Miscellaneous examples for Higher-Order Logic.

- HOLCF
Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic.

- HOLCF-FOCUS
FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321

- HOLCF-IMP
IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language.

- HOLCF-Library
- HOLCF-Tutorial
- HOLCF-ex
Miscellaneous examples for HOLCF.

- IOA
Author: Olaf Mueller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences.

- IOA-ABP
Author: Olaf Mueller The Alternating Bit Protocol performed in I/O-Automata.

- IOA-NTP
Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Mueller.

- IOA-Storage
Author: Olaf Mueller Memory storage case study.

- IOA-ex
Author: Olaf Mueller