# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1275400739 -7200
# Node ID 69b4eb4b12c626b41e015a2639453e580ad1981f
# Parent  54eea17575e6648da9b7ba9b936c4df87f40f3a7
added larry's quote

diff -r 54eea17575e6 -r 69b4eb4b12c6 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 01 15:48:25 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 01 15:58:59 2010 +0200
@@ -36,7 +36,11 @@
 section {* Introduction *}
 
 text {* 
-  {\hfill quote by Larry}\bigskip
+   \begin{flushright}
+  {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 
+    collect all the theorems we shall ever want into one giant list;''}\\
+    Paulson \cite{Paulson06}
+  \end{flushright}\smallskip
 
   \noindent
   Isabelle is a generic theorem prover in which many logics can be implemented. 
diff -r 54eea17575e6 -r 69b4eb4b12c6 Quotient-Paper/document/root.bib
--- a/Quotient-Paper/document/root.bib	Tue Jun 01 15:48:25 2010 +0200
+++ b/Quotient-Paper/document/root.bib	Tue Jun 01 15:58:59 2010 +0200
@@ -26,7 +26,7 @@
 
 @techreport{PVS:Interpretations,
         Author= {S. Owre and N. Shankar},
-        Title= {Theory Interpretations in PVS},
+        Title= {{T}heory {I}nterpretations in {PVS}},
         Number= {SRI-CSL-01-01},
         Institution= {Computer Science Laboratory, SRI International},
         Address= {Menlo Park, CA},
diff -r 54eea17575e6 -r 69b4eb4b12c6 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Tue Jun 01 15:48:25 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Tue Jun 01 15:58:59 2010 +0200
@@ -25,7 +25,7 @@
 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
+involved with quotient constructions, 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