FIXME-TODO
changeset 921 dae038c8cd69
parent 919 c46b6abad24b
child 952 9c3b3eaecaff
--- a/FIXME-TODO	Mon Jan 25 18:13:44 2010 +0100
+++ b/FIXME-TODO	Mon Jan 25 18:52:22 2010 +0100
@@ -4,6 +4,12 @@
 Higher Priority
 ===============
 
+- Ask Markus how the files Quot* should be named.
+  (There is a HOL/Library/Quotient.thy --- seems to be an example. *)
+
+- Is Bexeq the right name?
+
+
 - If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun