# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1328797090 -3600
# Node ID ed01965556901086a951b9789885ea8c6539f818
# Parent  c9633254a4ece7420f571d9aa625595bf330a202
qpaper-jv: merge and add to TODOs in the paper and in front.

diff -r c9633254a4ec -r ed0196555690 Quotient-Paper-jv/Paper.thy
--- a/Quotient-Paper-jv/Paper.thy	Thu Feb 09 14:47:24 2012 +0100
+++ b/Quotient-Paper-jv/Paper.thy	Thu Feb 09 15:18:10 2012 +0100
@@ -6,21 +6,6 @@
         "~~/src/HOL/Quotient_Examples/FSet"
 begin
 
-(****
-
-** things to do for the next version
-*
-* - what are quot_thms?
-* - what do all preservation theorems look like,
-    in particular preservation for quotient
-    compositions
-  - explain how Quotient R Abs Rep is proved (j-version)
-  - give an example where precise specification helps (core Haskell in nominal?)
-
-  - Mention Andreas Lochbiler in Acknowledgements and 'desceding'.
-
-*)
-
 notation (latex output)
   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
@@ -1330,14 +1315,17 @@
   package requires a substantial reasoning effort (see \cite{Paulson06}).
 
   {\bf \begin{itemize}
+  \item explain how Quotient R Abs Rep is proved
   \item Type maps and Relation maps (show the case for functions)
-  \item Quotient extensions
+  \item Quotient extensions (quot\_thms)
   \item Respectfulness and preservation
   - Show special cases for quantifiers and lambda
+  - How do prs theorems look like for quotient compositions
   \item Quotient-type locale
   - Show the proof as much simpler than Homeier's one
   \item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
   \item Lifting vs Descending vs quot\_lifted
+  - Mention Andreas Lochbiler in Acknowledgements
   - automatic theorem translation heuristic
   \item Partial equivalence quotients
   - Bounded abstraction
@@ -1348,6 +1336,8 @@
   injected and cleaned statement
   \item Examples of quotients and properties that we used the package for.
   \item co/contra-variance from Ondrej should be taken into account
+  \item give an example where precise specification of goal is necessary
+  \item mention multiple map\_prs2 theorems for compositional quotients
   \end{itemize}}
 *}