equal
deleted
inserted
replaced
6 |
6 |
7 |
7 |
8 Higher Priority |
8 Higher Priority |
9 =============== |
9 =============== |
10 |
10 |
11 - Ask Markus how the files Quot* should be named. |
|
12 (There is a HOL/Library/Quotient.thy --- seems to be an example. *) |
|
13 |
|
14 - If the constant definition gives the wrong definition |
11 - If the constant definition gives the wrong definition |
15 term, one gets a cryptic message about absrep_fun |
12 term, one gets a cryptic message about absrep_fun |
16 |
13 |
17 - Handle theorems that include Ball/Bex. For this, would |
14 - Handle theorems that include Ball/Bex. For this, would |
18 it help if we introduced separate Bex and Ball constants |
15 it help if we introduced separate Bex and Ball constants |
19 for quotienting? |
16 for quotienting? |
20 |
17 |
21 - The user should be able to give quotient_respects and |
18 - The user should be able to give quotient_respects and |
22 preserves theorems in a more natural form. |
19 preserves theorems in a more natural form. |
23 |
|
24 |
20 |
25 Lower Priority |
21 Lower Priority |
26 ============== |
22 ============== |
27 |
23 |
28 - accept partial equivalence relations |
24 - accept partial equivalence relations |
58 qconst :: "qty" |
54 qconst :: "qty" |
59 as "rconst" |
55 as "rconst" |
60 |
56 |
61 That means "qconst :: qty" is not read as a term, but |
57 That means "qconst :: qty" is not read as a term, but |
62 as two entities. |
58 as two entities. |
|
59 |
|
60 - Restrict automatic translation to particular quotient types |
|
61 |