--- 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 *}