# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276514662 -7200
# Node ID 8f493d371234dc04d892ea73996af6ba3157f0ed
# Parent  280b92df6a8b8fa3d56eb8f652ec1fd14f40463e
qpaper

diff -r 280b92df6a8b -r 8f493d371234 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 12:07:55 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 13:24:22 2010 +0200
@@ -871,15 +871,15 @@
   \item For lambda abstractions lambda preservation establishes
     the equality between the injected theorem and the goal. This allows both
     abstraction and quantification over lifted types.
-    @{thm [display] lambda_prs[no_vars]}
+    @{thm [display] (concl) lambda_prs[no_vars]}
   \item Relations over lifted types are folded with:
-    @{thm [display] Quotient_rel_rep[no_vars]}
+    @{thm [display] (concl) 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)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
+    @{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
   \end{itemize}
 
- Preservation of relations and user given constant preservation lemmas *}
+  *}
 
 section {* Examples *}