6 |
6 |
7 |
7 |
8 Higher Priority |
8 Higher Priority |
9 =============== |
9 =============== |
10 |
10 |
11 - Ask Markus how the files Quot* should be named. |
11 |
12 (There is a HOL/Library/Quotient.thy --- seems to be an example. *) |
12 - Also, in the interest of making nicer generated documentation, you |
|
13 might want to change all your "section" headings in Quotient.thy to |
|
14 "subsection", and add a "header" statement to the top of the file. |
|
15 Otherwise, each "section" gets its own chapter in the generated pdf, |
|
16 when the rest of HOL has one chapter per theory file (the chapter |
|
17 title comes from the "header" statement). |
13 |
18 |
14 - If the constant definition gives the wrong definition |
19 - If the constant definition gives the wrong definition |
15 term, one gets a cryptic message about absrep_fun |
20 term, one gets a cryptic message about absrep_fun |
16 |
21 |
17 - Handle theorems that include Ball/Bex. For this, would |
22 - Handle theorems that include Ball/Bex. For this, would |
18 it help if we introduced separate Bex and Ball constants |
23 it help if we introduced separate Bex and Ball constants |
19 for quotienting? |
24 for quotienting? |
20 |
25 |
21 - The user should be able to give quotient_respects and |
26 - The user should be able to give quotient_respects and |
22 preserves theorems in a more natural form. |
27 preserves theorems in a more natural form. |
23 |
|
24 |
28 |
25 Lower Priority |
29 Lower Priority |
26 ============== |
30 ============== |
27 |
31 |
28 - accept partial equivalence relations |
32 - accept partial equivalence relations |