diff -r fb201e383f1b -r da575186d492 Quotient-Paper-jv/TODO
--- a/Quotient-Paper-jv/TODO	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-Things to describe not in the original quotient paper:
-
-* Type maps and Relation maps (show the case for functions)
-* Quotient extensions
-* Respectfulness and preservation
-  - Show special cases for quantifiers and lambda
-* Quotient-type locale
-  - Show the proof as much simpler than Homeier's one
-* Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
-* Lifting vs Descending vs quot_lifted
-  - automatic theorem translation heuristic
-* Partial equivalence quotients
-  - Bounded abstraction
-  - Respects
-  - partial_descending
-* The heuristics for automatic regularization, injection and cleaning.
-* A complete example of a lifted theorem together with the regularized
-  injected and cleaned statement
-* Examples of quotients and properties that we used the package for.
-* co/contra-variance from Ondrej should be taken into account