# HG changeset patch # User Christian Urban # Date 1275084999 -7200 # Node ID bdbf040dce897a47083214c7905e0b4235381cf5 # Parent 4d8d9b8af76fd8489bb52fd40511a353b56d5c81 first version of the abstract diff -r 4d8d9b8af76f -r bdbf040dce89 Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Thu May 27 18:30:42 2010 +0200 +++ b/Quotient-Paper/document/root.tex Sat May 29 00:16:39 2010 +0200 @@ -20,9 +20,16 @@ \maketitle \begin{abstract} -Higher-order logic (HOL) is based on a safe logic kernel, which -can only be extended by introducing new definitions and new types. - +Higher-order logic (HOL) is based on a small logic kernel, whose +only mechanism for extension is the introduction of definitions +and types. Both extensions are often performed by +quotient constructions, for example finite sets are constructed by quotienting +lists, or integers by quotienting pairs of natural numbers. To ease the work +involved with quotient construction, we re-implemented in Isabelle/HOL +the quotient package by Homeier. In doing so we extended his work +in order to deal with compositions of quotients. Also, we designed +our quotient package so that every step in a quotient construction +can be performed separately. \end{abstract} % generated text of all theories