diff -r 781fbc8c0591 -r 6cfb5d8a5b5b Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Nov 07 11:22:31 2010 +0000
+++ b/Quotient-Paper/Paper.thy	Wed Nov 10 13:40:46 2010 +0000
@@ -138,12 +138,12 @@
   Quotients are important in a variety of areas, but they are really ubiquitous in
   the area of reasoning about programming language calculi. A simple example
   is the lambda-calculus, whose raw terms are defined as
-  %
-  %\begin{isabelle}\ \ \ \ \ %%%
+  
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda}
-  %\end{isabelle}
-  %
-  %\noindent
+  \end{isabelle}
+  
+  \noindent
   The problem with this definition arises, for instance, when one attempts to
   prove formally the substitution lemma \cite{Barendregt81} by induction
   over the structure of terms. This can be fiendishly complicated (see
@@ -151,7 +151,7 @@
   about raw lambda-terms). In contrast, if we reason about
   $\alpha$-equated lambda-terms, that means terms quotient according to
   $\alpha$-equivalence, then the reasoning infrastructure provided, 
-  for example, by Nominal Isabelle %\cite{UrbanKaliszyk11}
+  for example, by Nominal Isabelle %%\cite{UrbanKaliszyk11}
   makes the formal 
   proof of the substitution lemma almost trivial. 
 
@@ -262,7 +262,7 @@
   \end{isabelle}
 
   \noindent
-  where @{text "@"} is %the usual 
+  where @{text "@"} is the usual 
   list append. We expect that the corresponding 
   operator on finite sets, written @{term "fconcat"},
   builds finite unions of finite sets:
@@ -317,8 +317,8 @@
   sketch this part of our work in Section 5 and we defer the reader to a longer
   version for the details. However, we will give in Section 3 and 4 all 
   definitions that specify the input and output data of our three-step 
-  lifting procedure.
-  %Appendix A gives an example how our quotient package works in practise.
+  lifting procedure. Appendix A gives an example how our quotient 
+  package works in practise.
 *}
 
 section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
@@ -690,7 +690,7 @@
   In our implementation we further
   simplify this function by rewriting with the usual laws about @{text
   "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
-  id \<circ> f = f"}. This gives us %%%the simpler abstraction function
+  id \<circ> f = f"}. This gives us the simpler abstraction function
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
@@ -709,12 +709,12 @@
   distinguish between arguments and results, but can deal with them uniformly.
   Consequently, all definitions in the quotient package 
   are of the general form
-  %
-  %\begin{isabelle}\ \ \ \ \ %%%
+  
+  \begin{isabelle}\ \ \ \ \ %%%
   \mbox{@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}}
-  %\end{isabelle}
-  %
-  %\noindent
+  \end{isabelle}
+  
+  \noindent
   where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
   type of the defined quotient constant @{text "c"}. This data can be easily
   generated from the declaration given by the user.
@@ -758,7 +758,7 @@
   two restrictions in form of proof obligations that arise during the
   lifting. The reason is that even if definitions for all raw constants 
   can be given, \emph{not} all theorems can be lifted to the quotient type. Most 
-  notable is the bound variable function %%, that is the constant @{text bn}, 
+  notable is the bound variable function, that is the constant @{text bn}, 
   defined 
   for raw lambda-terms as follows
 
@@ -812,12 +812,12 @@
   lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
   constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation 
   we generate the following proof obligation
-  %
-  %\begin{isabelle}\ \ \ \ \ %%%
+  
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.
-  %\end{isabelle}
-  %
-  %\noindent
+  \end{isabelle}
+  
+  \noindent
   Homeier calls these proof obligations \emph{respectfulness
   theorems}. However, unlike his quotient package, we might have several
   respectfulness theorems for one constant---he has at most one.
@@ -829,12 +829,12 @@
   Before lifting a theorem, we require the user to discharge
   respectfulness proof obligations. In case of @{text bn}
   this obligation is %%as follows
-  % 
-  %\begin{isabelle}\ \ \ \ \ %%%
+   
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text  "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
-  %\end{isabelle}
-  %
-  %\noindent
+  \end{isabelle}
+  
+  \noindent
   and the point is that the user cannot discharge it: because it is not true. To see this,
   we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} 
   using extensionality to obtain the false statement
@@ -1242,15 +1242,20 @@
 
   \noindent
   {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
-  discussions about his HOL4 quotient package.\\[-5mm]% and explaining to us
-  %some of its finer points in the implementation. Without his patient
-  %help, this work would have been impossible.
+  discussions about his HOL4 quotient package and explaining to us
+  some of its finer points in the implementation. Without his patient
+  help, this work would have been impossible.
+*}
 
-%  \appendix
+text_raw {*
+  %%\bibliographystyle{abbrv}
+  \bibliography{root}
+
+  \appendix
 
 *}
 
-(* section {* Examples \label{sec:examples} *}
+section {* Examples \label{sec:examples} *}
 
 text {*
 
@@ -1341,7 +1346,7 @@
   Although seemingly simple, arriving at this result without the help of a quotient
   package requires a substantial reasoning effort (see \cite{Paulson06}).
 *}
-*)
+
 
 
 (*<*)