14 text {* TBD *}

    14 text {* 

    15   Isabelle is a generic theorem prover in which many logics can be implemented. 

    16   The most widely used one, however, is

    17   Higher-Order Logic (HOL). This logic consists of a small number of 

    18   axioms and inference

    19   rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted 

    20   mechanisms for extending the logic: one is the definition of new constants

    21   in terms of existing ones; the other is the introduction of new types

    22   by identifying non-empty subsets in existing types. It is well understood 

    23   to use both mechanism for dealing with quotient constructions in HOL (cite Larry).

    24   For example the integers in Isabelle/HOL are constructed by a quotient construction over 

    25   the type @{typ "nat \<times> nat"} and the equivalence relation

    26 

    27   @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}

    28 

    29   \noindent

    30   The problem is that one 

    31   

    32 

    33 

    34 *}