equal
deleted
inserted
replaced
22 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
22 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
23 \institute{$^*$ Technical University of Munich, Germany} |
23 \institute{$^*$ Technical University of Munich, Germany} |
24 \maketitle |
24 \maketitle |
25 |
25 |
26 \begin{abstract} |
26 \begin{abstract} |
27 Higher-order logic (HOL), used in several theorem provers, is based on a small |
27 Higher-order logic (HOL), used in a number of theorem provers, is based on a small |
28 logic kernel, whose only mechanism for extension is the introduction of safe |
28 logic kernel, whose only mechanism for extension is the introduction of safe |
29 definitions and non-empty types. Both extensions are often performed by |
29 definitions and non-empty types. Both extensions are often performed by |
30 quotient constructions; for example finite sets are constructed by quotienting |
30 quotient constructions; for example finite sets are constructed by quotienting |
31 lists, or integers by quotienting pairs of natural numbers. To ease the work |
31 lists, or integers by quotienting pairs of natural numbers. To ease the work |
32 involved with quotient constructions, we re-implemented in Isabelle/HOL the |
32 involved with quotient constructions, we re-implemented in Isabelle/HOL the |