# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1275399967 -7200
# Node ID 118a0ca16381e87edad5dd3939dbfe2b2ac74ea1
# Parent  86c977b4a9bbcb62249e264598700824d6f45b15# Parent  530b0adbcf77db8561edf106f89295eec7076aa7
merged

diff -r 86c977b4a9bb -r 118a0ca16381 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Jun 01 15:21:01 2010 +0200
+++ b/Paper/Paper.thy	Tue Jun 01 15:46:07 2010 +0200
@@ -937,8 +937,8 @@
 
   \noindent
   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
-  and \isacommand{bind\_res} the binding clauses will make a difference to the semantics
-  of the specification (the corresponding alpha-equivalence will differ). We will 
+  and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
+  of the specifications (the corresponding alpha-equivalence will differ). We will 
   show this later with an example.
   
   There are some restrictions we need to impose on binding clasues: First, a
@@ -1058,7 +1058,6 @@
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
   inside the assignment. This difference has consequences for the free-variable 
   function and alpha-equivalence relation, which we are going to define below.
-  
   For this definition, we have to impose some restrictions on deep binders. First,
   we cannot have more than one binding function for one binder. So we exclude:
 
diff -r 86c977b4a9bb -r 118a0ca16381 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Tue Jun 01 15:21:01 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Tue Jun 01 15:46:07 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