# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276503279 -7200
# Node ID 5e98b3f231a03a424e15270d09e291edc23fed49
# Parent  3f480e33d8df4b60e6e66d4b9bd49d97cdeb7b76
qpaper / minor

diff -r 3f480e33d8df -r 5e98b3f231a0 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 09:28:52 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 10:14:39 2010 +0200
@@ -835,14 +835,15 @@
   Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
   in the injected theorem we can use the theorem:
 
-  @{thm [display] rep_abs_rsp[no_vars]}
+  @{thm [display, indent=10] rep_abs_rsp[no_vars]}
 
+  \noindent
   and continue the proof.
 
   Otherwise we introduce an appropriate relation between the subterms and continue with
   two subgoals using the lemma:
 
-  @{thm [display] apply_rsp[no_vars]}
+  @{thm [display, indent=10] apply_rsp[no_vars]}
 
 *}
 
@@ -864,7 +865,7 @@
     @{thm [display] Quotient_rel_rep[no_vars]}
   \item User given preservation theorems, that allow using higher level operations
     and containers of types being lifted. An example may be
-    @{thm [display] map_prs(1)[no_vars]}
+    @{thm [display] map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
   \end{itemize}
 
  Preservation of relations and user given constant preservation lemmas *}
@@ -951,13 +952,15 @@
   \begin{itemize}
 
   \item Peter Homeier's package~\cite{Homeier05} (and related work from there)
+
   \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems
     but only first order.
 
   \item PVS~\cite{PVS:Interpretations}
   \item MetaPRL~\cite{Nogin02}
-  \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,
-    Dixon's FSet, \ldots)
+
+%  \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,
+%    Dixon's FSet, \ldots)
 
   \item Oscar Slotosch defines quotient-type automatically but no
     lifting~\cite{Slotosch97}.