This module extends the boolean-related theory by giving definitions for classic predicate logic theory objects not introduced in 'CoreThry', and adds various derived syntax functions, theorems and inference rules. Note that derivations relying on the Axiom of Choice are separated out into the 'BoolClass' module.

This module proves various algebraic property theorems for the predicate logic operators.

This module derives further predicate logic theorems and inference rules. Unlike all preceding derivations, these all use the Axiom of Choice (i.e. 'select_ax'), and thus could be considered as classical logic. However, note that some of these (such as 'exists_rule') are actually derivable in intuitionistic logic if an alternative definition of existential quantification is used (as in HOL Light).

This module completes the logical core for HOL by defining the core theory. This involves giving declarations, definitions and axioms for all the HOL theory objects anticipated by the language and inference kernels.

This module defines a command for defining type bijection constants for a given type constant definition.

This module defines two specialised forms of definition for function constants. The first form is for non-recursive functions and the second is for recursive functions.

Questo modulo costituisce una libreria di operazioni su alberi dinamici di ricerca - alberi binari auto-bilanciati che memorizzano informazioni su nodi ordinati in base a un indice rispetto alla relazione (<).

This module implements the display modes mechanism, for configuring how the pretty printers display types and terms. Note that the display modes make no difference to the way that types and terms are parsed.

This module implements equality congruence rules for equality, function application and predicate logic operators. These are all trivial derivations of the primitive congruence rules 'mk_comb_rule' and 'mk_abs_rule' (see 'Thm' module) and the derived congruence rules 'mk_comb1_rule' and 'mk_comb2_rule' (see 'Equal' module).

This module adds more constants and inference rules for basic reasoning using equality.

Questo modulo definisce tre nuove eccezioni di uso generale, insieme a una stampa di queste eccezioni.

This module extends the HOL logic with an infinite-cardinality base type, together with a zero and a successor function for this type. These get used in the 'Nat' module as the basis for defining the natural numbers.

This module implements the lexical analysis stage, common to both HOL type and term quotation parsing. The top-level type and term parsers are implemented in the 'Parser' module. The classification of characters, used to determine how lexical tokens are formed, is implemented in the 'Names' module.

Questo modulo definisce varie utilità di programmazione funzionale da usare nel corso dell'implementazione.

This module provides support for classifying HOL names for the purposes of parsing and printing. This consists of tests for basic classes of name and commands for setting identifier fixity and enumeration brackets. This module is a trusted component of the system, since it is used in the implementation of the pretty printer.

This module extends the HOL logic with the theory of natural numbers. This involves giving theory object definitions for the naturals base type and the "ZERO" and "SUC" constants, based on the theory of individuals, and proving a few important properties.

This module defines some classic natural number arithmetic operators, using recursive function definition and the "SUC" and "ZERO" constants, and proves various basic properties about each operator.

This module defines conversions for evaluating arithmetic operations on natual number numerals. Because large proofs may involve heavy numeric computation, special consideration is given to the efficieny of these functions.

This module defines the representation of natural number numerals. This is based on the HOL functions "BIT0" and "BIT1".

This module defines the classic natural number arithmetic relations and derives various basic properties about them.

This module extends the HOL logic with the theory of ordered pairs. This involves giving theory object definitions for the product type operator, the pairing function and the constants "FST" and "SND", and proving a few basic properties. Syntax functions and equality congruence rules are also provided.

This module implements syntax analysis and top-level parsing of type/term quotations into internal types/terms. The syntax analysis functions take a list of lexical tokens as their source, and return a pretype/preterm that gets passed on to type analysis. Lexical analysis is implemented in the 'Lexer' module, and type analsyis (actually common to parsing and printing) is implemented in the 'TypeAnal' module.

This module defines the pretype and preterm datatypes (called 'pretype' and 'preterm'), and various basic operations on them. These are used during parsing and printing as intermediate representations of types/terms between their quotation and internal representations. They incorporate extra datatype classes, that don't occur in the corresponding internal datatypes and are only used during parsing and printing. Being intermediate datatypes, there is no need for well-formedness restrictions on their constructors, and so the datatypes are not made abstract.

This module implements the type, term and theorem pretty printers, for outputting quotation representations of internal types/terms/theorems. The printers take into account identifier fixity status and enumeration bracket settings (see 'Names' module), certain special-case theory objects (whose declarations in later modules are anticipated here), and the display modes (see 'DModes' module). This module is a trusted component of the system, since the user will normally rely on it to determine what has been proved and what has been asserted.

This module provides library support for generic reader functions that process data from a given source and return a read item and the source correspondingly advanced, ready for the next item to be read. This gets used in the HOL quotation lexer and parsers (see 'Lexer' and 'Parser' modules respectively).

This module implements databases for storing theorems and lemmas under a name index. Like axioms, stored theorems are restricted to having no free variables or assumptions, whereas stored lemmas are theorems that have no such restrictions.

This module defines the internal representation of HOL terms. This is done by defining an abstract datatype for terms, and then primitive syntax functions for constructing and destructing terms, and support for constant declaration. The primitive syntax constructors ensure that only well- formed terms can be constructed. This module is a trusted component of the system.

This module defines the basic mechanisms for logical deduction and theory assertion. As is characteristic of LCF-style theorem provers, this is done by defining an abstract datatype for the internal representation of HOL theorems. The primitive constructors for this datatype are limited to the primitive inference rules and the primitive assertion commands. Any subsequent theorem-creating functions must ultimately be implemented in terms of these constructors. This module is a trusted component of the system.

This module defines the internal representation of HOL types. This is done by defining an abstract datatype for types, and then primitive syntax functions for constructing and destructing types, and support for type constant declaration. The primitive syntax constructors ensure that only well-formed types can be constructed. This module is a trusted component

This module defines type analysis routines for pretypes and preterms, used in parsing and printing type/term quotations. The primary routines are detyping, type unification, type inference and type consistency check. This module is used in the implementation of the pretty printer, and is a trusted component of the system.

This module defines type analysis routines for pretypes and preterms, used in parsing and printing type/term quotations. The primary routines are detyping, type unification, type inference and type consistency check. This module is used in the implementation of the pretty printer, and is a trusted component of the system.

This module defines various basic operations on types and terms that get used in the implementation of the primitive inference rules and primitive assertion commands in the 'Thm' module. This module is a trusted component of the system.

This module defines various basic useful operations on types, terms and theorems.

The primitive inference rules and theory commands have minimal, stripped- down functionality, to make the language and inference kernels as concise as possible and their correctness as easy as possible to justify. This module adds basic wrappers around these primitives, giving the rules step counting and the theory commands benign redefinition and slightly enhanced functionality.