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