equal
deleted
inserted
replaced
18 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
18 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
19 \institute{$^*$ Technical University of Munich, Germany} |
19 \institute{$^*$ Technical University of Munich, Germany} |
20 \maketitle |
20 \maketitle |
21 |
21 |
22 \begin{abstract} |
22 \begin{abstract} |
23 Higher-order logic (HOL) is based on a safe logic kernel, which |
23 Higher-order logic (HOL) is based on a small logic kernel, whose |
24 can only be extended by introducing new definitions and new types. |
24 only mechanism for extension is the introduction of definitions |
25 |
25 and types. Both extensions are often performed by |
|
26 quotient constructions, for example finite sets are constructed by quotienting |
|
27 lists, or integers by quotienting pairs of natural numbers. To ease the work |
|
28 involved with quotient construction, we re-implemented in Isabelle/HOL |
|
29 the quotient package by Homeier. In doing so we extended his work |
|
30 in order to deal with compositions of quotients. Also, we designed |
|
31 our quotient package so that every step in a quotient construction |
|
32 can be performed separately. |
26 \end{abstract} |
33 \end{abstract} |
27 |
34 |
28 % generated text of all theories |
35 % generated text of all theories |
29 \input{session} |
36 \input{session} |
30 |
37 |